ι : Type ?u.28195
α : Type u_1
β : Type ?u.28201
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : T1Space α
s : Opens α
⊢ IsAtom (↑toDual (Closeds.compl (compl s))) ↔ ∃ x, Closeds.compl (compl s) = Closeds.compl (Closeds.singleton x)
ι : Type ?u.28195
α : Type u_1
β : Type ?u.28201
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : T1Space α
s : Opens α
⊢ IsCoatom s ↔ ∃ x, s = Closeds.compl (Closeds.singleton x)
rw [← s.compl_compl, ← isAtom_dual_iff_isCoatom]
ι : Type ?u.28195
α : Type u_1
β : Type ?u.28201
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : T1Space α
s : Opens α
⊢ IsAtom (↑(Closeds.complOrderIso α) (compl s)) ↔ ∃ x, Closeds.compl (compl s) = Closeds.compl (Closeds.singleton x)
ι : Type ?u.28195
α : Type u_1
β : Type ?u.28201
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : T1Space α
s : Opens α
⊢ IsAtom (↑toDual (Closeds.compl (compl s))) ↔ ∃ x, Closeds.compl (compl s) = Closeds.compl (Closeds.singleton x)
change IsAtom (Closeds.complOrderIso α s.compl) ↔ _
no goals
ι : Type ?u.28195
α : Type u_1
β : Type ?u.28201
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : T1Space α
s : Opens α
⊢ IsAtom (↑(Closeds.complOrderIso α) (compl s)) ↔ ∃ x, Closeds.compl (compl s) = Closeds.compl (Closeds.singleton x)
simp only [(Closeds.complOrderIso α).isAtom_iff, Closeds.isAtom_iff,
  Closeds.compl_bijective.injective.eq_iff]