α : Type u
β : Type v
ι : Type ?u.184023
π : ι → Type ?u.184028
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s✝ t s : Set α
H : s ∈ irreducibleComponents α
⊢ s = closure s
α : Type u
β : Type v
ι : Type ?u.184023
π : ι → Type ?u.184028
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s✝ t s : Set α
H : s ∈ irreducibleComponents α
⊢ IsClosed s
rw [← closure_eq_iff_isClosed, eq_comm]
no goals
α : Type u
β : Type v
ι : Type ?u.184023
π : ι → Type ?u.184028
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s✝ t s : Set α
H : s ∈ irreducibleComponents α
⊢ s = closure s
exact subset_closure.antisymm (H.2 H.1.closure subset_closure)