Theorem: Nonseparating.empty (Ray/AnalyticManifold/Nonseparating.lean)

State before:
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
S : Type
inst✝² : TopologicalSpace S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
⊢ Dense ∅ᶜ
Tactic:
simp only [compl_empty, dense_univ]
State after:
no goals

State before:
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
S : Type
inst✝² : TopologicalSpace S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
⊢ ∀ (x : X) (u : Set X), x ∈ ∅ → u ∈ 𝓝 x → ∃ c ⊆ u \ ∅, c ∈ 𝓝[∅ᶜ] x ∧ IsPreconnected c
Tactic:
simp only [mem_empty_iff_false, IsEmpty.forall_iff, forall_const, imp_true_iff]
State after:
no goals