α : Type u_1
β : Type ?u.81807
s : Set α
⊢ (∃ x, sᶜ = {x}) ↔ ∃ x, s = {x}ᶜ
α : Type u_1
β : Type ?u.81807
s : Set α
⊢ IsCoatom s ↔ ∃ x, s = {x}ᶜ
rw [isCompl_compl.isCoatom_iff_isAtom, isAtom_iff]
no goals
α : Type u_1
β : Type ?u.81807
s : Set α
⊢ (∃ x, sᶜ = {x}) ↔ ∃ x, s = {x}ᶜ
simp_rw [@eq_comm _ s, compl_eq_comm]