English
A partial order on the idempotent-pairs set is established consistent with the lattice structure and complement operation.
Русский
Установлен частичный порядок на множество пар идемпотентности, согласованный с структурой латтис и операцией дополнения.
LaTeX
$$$\le$ is defined compatibly with the lattice structure on E.$$
Lean4
instance : BooleanAlgebra { a : R // IsIdempotentElem a }
where
__ :
DistribLattice
_ :=
.ofInfSupLe fun a b c ↦
Eq.le <|
Subtype.ext <|
by
simp_rw [(· ⊔ ·), (· ⊓ ·), SemilatticeSup.sup, SemilatticeInf.inf, Lattice.inf, SemilatticeInf.inf, mul_sub,
mul_add, mul_mul_mul_comm]
rw [a.2]
__ : OrderTop _ := inferInstance
__ : OrderBot _ := inferInstance
compl a := ⟨_, a.2.one_sub⟩
inf_compl_le_bot a := (mul_zero _).trans ((mul_one_sub ..).trans <| by rw [a.2, sub_self]).symm
top_le_sup_compl
a :=
(one_mul _).trans <| by
simp_rw [(· ⊔ ·), SemilatticeSup.sup, add_sub_cancel, mul_sub, mul_one]
rw [a.2, sub_self, sub_zero]; rfl
sdiff_eq _ _ := rfl
himp a b := ⟨_, (a.2.mul b.2.one_sub).one_sub⟩
himp_eq a
b :=
Subtype.ext <| by
simp_rw [(· ⊔ ·), SemilatticeSup.sup, add_comm b.1, add_sub_assoc, mul_sub, mul_one, sub_sub_cancel, sub_add,
mul_comm]
