ι : Type ?u.25211
α : Type u_1
β : Type ?u.25217
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : T1Space α
s : Closeds α
this : IsAtom ↑s ↔ IsAtom s
⊢ IsAtom s ↔ ∃ x, s = singleton x
ι : Type ?u.25211
α : Type u_1
β : Type ?u.25217
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : T1Space α
s : Closeds α
⊢ IsAtom s ↔ ∃ x, s = singleton x
have : IsAtom (s : Set α) ↔ IsAtom s := by
  refine' Closeds.gi.isAtom_iff' rfl (fun t ht => _) s
  obtain ⟨x, rfl⟩ := t.isAtom_iff.mp ht
  exact closure_singleton
no goals
ι : Type ?u.25211
α : Type u_1
β : Type ?u.25217
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : T1Space α
s : Closeds α
this : IsAtom ↑s ↔ IsAtom s
⊢ IsAtom s ↔ ∃ x, s = singleton x
simp only [← this, (s : Set α).isAtom_iff, SetLike.ext'_iff, Closeds.singleton_coe]
ι : Type ?u.25211
α : Type u_1
β : Type ?u.25217
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : T1Space α
s : Closeds α
t : Set α
ht : IsAtom t
⊢ ↑(Closeds.closure t) = t
ι : Type ?u.25211
α : Type u_1
β : Type ?u.25217
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : T1Space α
s : Closeds α
⊢ IsAtom ↑s ↔ IsAtom s
refine' Closeds.gi.isAtom_iff' rfl (fun t ht => _) s
case intro
ι : Type ?u.25211
α : Type u_1
β : Type ?u.25217
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : T1Space α
s : Closeds α
x : α
ht : IsAtom {x}
⊢ ↑(Closeds.closure {x}) = {x}
ι : Type ?u.25211
α : Type u_1
β : Type ?u.25217
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : T1Space α
s : Closeds α
t : Set α
ht : IsAtom t
⊢ ↑(Closeds.closure t) = t
obtain ⟨x, rfl⟩ := t.isAtom_iff.mp ht
no goals
case intro
ι : Type ?u.25211
α : Type u_1
β : Type ?u.25217
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : T1Space α
s : Closeds α
x : α
ht : IsAtom {x}
⊢ ↑(Closeds.closure {x}) = {x}
exact closure_singleton