English
The subtype {P : M // IsLprojection X P} carries a Boolean algebra structure with complement and sdiff, satisfying standard Boolean identities (inf_compl_le_bot, top_le_sup_compl, sdiff_eq, etc.).
Русский
Подтип содержит булову алгебру с дополнением и разностью, удовлетворяющую стандартным тождствам булевой алгебры.
LaTeX
$$BooleanAlgebra IsLprojection.Subtype$$
Lean4
instance BooleanAlgebra [FaithfulSMul M X] : BooleanAlgebra { P : M // IsLprojection X P } :=
{ IsLprojection.Subtype.hasCompl, IsLprojection.Subtype.sdiff,
IsLprojection.Subtype.boundedOrder with
inf_compl_le_bot := fun P => (Subtype.ext (by rw [coe_inf, coe_compl, coe_bot, ← coe_compl, mul_compl_self])).le
top_le_sup_compl := fun P =>
(Subtype.ext (by rw [coe_top, coe_sup, coe_compl, add_sub_cancel, ← coe_compl, mul_compl_self, sub_zero])).le
sdiff_eq := fun P Q => Subtype.ext <| by rw [coe_sdiff, ← coe_compl, coe_inf] }
