English
Further properties of the Boolean algebra on E hold, providing alternate proofs of the same structure and relations as in item 27284.
Русский
Дополнительные свойства буловой алгебры на E, подтверждающие существование альтернативных доказательств той же структуры.
LaTeX
$$$\text{Boolean algebra on } E\text{ with }compl(a)= (b,a)\text{ and }top,bottom\text{ as in (27284)}$$$
Lean4
instance {S : Type*} [CommSemigroup S] : SemilatticeInf { a : S // IsIdempotentElem a }
where
le a b := a.1 * b = a
le_refl a := a.2
le_trans a b c hab hbc := show _ = _ by rw [← hab, mul_assoc, hbc]
le_antisymm a b hab hba := Subtype.ext <| by rw [← hab, mul_comm, hba]
inf a b := ⟨_, a.2.mul b.2⟩
inf_le_left a b := show _ = _ by simp_rw [mul_right_comm]; rw [a.2]
inf_le_right a b := show _ = _ by simp_rw [mul_assoc]; rw [b.2]
le_inf a b c hab hac := by simp_rw [← mul_assoc]; rw [hab, hac]
