partialOrder — Mathlib

English

The product of two L-projections with a faithful action is again an L-projection.

Русский

Произведение двух L-проекций при верном действии скаляров снова является L-проекцией.

LaTeX

$$If $P,Q$ are L-projections with faithful scalar action, then $P\\cdot Q$ is an L-projection.$$

Lean4

instance partialOrder [FaithfulSMul M X] : PartialOrder { P : M // IsLprojection X P }
    where
  le P Q := (↑P : M) = ↑(P ⊓ Q)
  le_refl P := by simpa only [coe_inf, ← sq] using P.prop.proj.eq.symm
  le_trans P Q R h₁
    h₂ := by
    simp only [coe_inf] at h₁ h₂ ⊢
    rw [h₁, mul_assoc, ← h₂]
  le_antisymm P Q h₁ h₂ := Subtype.eq (by convert (P.prop.commute Q.prop).eq)

Похожие утверждения