ι : Type ?u.55295
α : Type u_1
β : Type ?u.55301
π : ι → Type ?u.55306
inst✝ : CoheytingAlgebra α
a : α
⊢ ⊤ ≤ ￢a ⊔ a
ι : Type ?u.55295
α : Type u_1
β : Type ?u.55301
π : ι → Type ?u.55306
inst✝ : CoheytingAlgebra α
a : α
⊢ (￢a) ∆ a = ⊤
rw [eq_top_iff, symmDiff, hnot_sdiff, sup_sdiff_self]
no goals
ι : Type ?u.55295
α : Type u_1
β : Type ?u.55301
π : ι → Type ?u.55306
inst✝ : CoheytingAlgebra α
a : α
⊢ ⊤ ≤ ￢a ⊔ a
exact Codisjoint.top_le codisjoint_hnot_left