English
Let R be a commutative monoid with addition. Consider the set E of all pairs (a,b) in R×R such that a·b = 0 and a + b = 1. Then the map that swaps coordinates, compl(a) = (b,a), defines a complementation operation on E, giving a Boolean algebra structure on E.
Русский
Пусть R — коммутативная моноида с сложением. Рассмотрим множество E из пар (a,b) ∈ R×R таких, что a·b = 0 и a + b = 1. Замена координат compl(a,b) = (b,a) задаёт операцию дополнения на E, образуя булову алгебру на E.
LaTeX
$$$E = \{(a,b) \in R \times R \mid a b = 0 \land a + b = 1\}.\quad \operatorname{compl}: E \to E,\; \operatorname{compl}(a,b) = (b,a)$ является дополнением в буловой алгебре на $E$.$$
Lean4
instance [CommMonoid R] [AddCommMonoid R] : HasCompl { a : R × R // a.1 * a.2 = 0 ∧ a.1 + a.2 = 1 } where
compl a := ⟨(a.1.2, a.1.1), (mul_comm ..).trans a.2.1, (add_comm ..).trans a.2.2⟩
