English
If M acts faithfully on X, then the subtype {P ∈ M | IsLprojection X P} forms a lattice under sup/inf with sup = max and inf = min in M.
Русский
Если действие M на X верно-faithful, то подмножество {P ∈ M | IsLprojection X P} образует решётку, где операция наибольшее/наименьшее соответствует максимуму/минимуму в M.
LaTeX
$$\text{If } [FaithfulSMul M X], \{ P : M // IsLprojection X P \} \text{ is a lattice with } \sup = \max, \inf = \min.$$
Lean4
instance [FaithfulSMul M X] : Lattice { P : M // IsLprojection X P }
where
sup := max
inf := min
le_sup_left P
Q := by rw [le_def, coe_inf, coe_sup, ← add_sub, mul_add, mul_sub, ← mul_assoc, P.prop.proj.eq, sub_self, add_zero]
le_sup_right P
Q := by
rw [le_def, coe_inf, coe_sup, ← add_sub, mul_add, mul_sub, (P.prop.commute Q.prop).eq, ← mul_assoc, Q.prop.proj.eq,
add_sub_cancel]
sup_le P Q
R :=
by
rw [le_def, le_def, le_def, coe_inf, coe_inf, coe_sup, coe_inf, coe_sup, ← add_sub, add_mul, sub_mul, mul_assoc]
intro h₁ h₂
rw [← h₂, ← h₁]
inf_le_left P
Q := by rw [le_def, coe_inf, coe_inf, coe_inf, mul_assoc, (Q.prop.commute P.prop).eq, ← mul_assoc, P.prop.proj.eq]
inf_le_right P Q := by rw [le_def, coe_inf, coe_inf, coe_inf, mul_assoc, Q.prop.proj.eq]
le_inf P Q
R := by
rw [le_def, le_def, le_def, coe_inf, coe_inf, coe_inf, coe_inf, ← mul_assoc]
intro h₁ h₂
rw [← h₁, ← h₂]
