no goals
X : Type ?u.8941
α : Type u_1
α' : Type ?u.8947
β : Type u_2
γ : Type ?u.8953
δ : Type ?u.8956
M : Type ?u.8959
E : Type ?u.8962
R : Type ?u.8965
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace α'
inst✝² : One β
inst✝¹ : One γ
inst✝ : One δ
g : β → γ
f : α → β
f₂ : α → γ
m : β → γ → δ
x : α
⊢ HasCompactMulSupport f ↔ IsCompact (closure (mulSupport f))
rfl