α : Type u_1
inst✝ : TopologicalSpace α
ι : Type ?u.465
⊢ ∅ = ∅ ∨ ∃ f, Continuous f ∧ range f = ∅
α : Type u_1
inst✝ : TopologicalSpace α
ι : Type ?u.465
⊢ AnalyticSet ∅
rw [AnalyticSet]
no goals
α : Type u_1
inst✝ : TopologicalSpace α
ι : Type ?u.465
⊢ ∅ = ∅ ∨ ∃ f, Continuous f ∧ range f = ∅
exact Or.inl rfl