English
There is a Boolean algebra structure on E, with operations ∧, ∨, ⟂ defined coordinatewise via the underlying algebraic operations, plus top and bottom as the natural idempotent corners.
Русский
Существует булова алгебра над множеством E, операции ∧, ∨, ⟂ задаются координатно через базовые операции; верх и низ соответствуют естественным константам идемпотентного разложения.
LaTeX
$$$E \\text{ с }\land, \\lor, \\lnot \\text{ образует булову алгебру; }top=(1,0), bottom=(0,1)$$$
Lean4
instance : BooleanAlgebra { a : R × R // a.1 * a.2 = 0 ∧ a.1 + a.2 = 1 }
where
inf a b := (aᶜ ⊔ bᶜ)ᶜ
inf_le_left a
b := by
simp_rw [(· ≤ ·), (· ⊔ ·), (·ᶜ), SemilatticeSup.sup, mul_right_comm, (IsIdempotentElem.of_mul_add a.2.1 a.2.2).1.eq]
inf_le_right a
b := by
simp_rw [(· ≤ ·), (· ⊔ ·), (·ᶜ), SemilatticeSup.sup, mul_assoc, (IsIdempotentElem.of_mul_add b.2.1 b.2.2).1.eq]
le_inf a b c hab hac := by simp_rw [(· ≤ ·), (· ⊔ ·), (·ᶜ), SemilatticeSup.sup, ← mul_assoc]; rw [hab, hac]
le_sup_inf a b
c :=
Eq.le <|
mul_eq_zero_add_eq_one_ext_right <| by
simp_rw [(· ⊔ ·), (· ⊓ ·), (·ᶜ), SemilatticeSup.sup, add_mul, mul_add, mul_mul_mul_comm _ b.1.1,
(IsIdempotentElem.of_mul_add a.2.1 a.2.2).2.eq, ← mul_assoc, a.2.1, zero_mul, zero_add]
top := ⟨(1, 0), mul_zero _, add_zero _⟩
bot := ⟨(0, 1), zero_mul _, zero_add _⟩
inf_compl_le_bot
a :=
Eq.le <|
mul_eq_zero_add_eq_one_ext_right <| by
simp_rw [(· ⊔ ·), (· ⊓ ·), (·ᶜ), SemilatticeSup.sup, (IsIdempotentElem.of_mul_add a.2.1 a.2.2).1.eq, add_comm,
a.2.2]
top_le_sup_compl
a :=
Eq.le <|
mul_eq_zero_add_eq_one_ext_left <| by
simp_rw [(· ⊔ ·), (·ᶜ), SemilatticeSup.sup, (IsIdempotentElem.of_mul_add a.2.1 a.2.2).2.eq, a.2.2]
le_top _ := mul_one _
bot_le _ := zero_mul _
sdiff_eq _ _ := rfl
himp_eq _ _ := rfl
