one — Mathlib

English

The set of L-projections on X inside M has a multiplicative identity, namely the element of M given by 1, which itself satisfies the L-projection condition. In particular, the unit of M restricts to a unit in the subobject {P ∈ M | IsLprojection X P}.

Русский

Множество L-проекций на X внутри M образует единичный элемент относительно умножения, равный 1, который сам удовлетворяет условию L-проекции. Единица M ограничивается до единицы в подобъекте {P ∈ M | IsLprojection X P}.

LaTeX

$$$1 \in \{ P \in M \;|\; \IsLprojection(X,P) \}.$$$

Lean4

instance one : One { P : M // IsLprojection X P } :=
  ⟨⟨1, sub_zero (1 : M) ▸ (0 : { P : M // IsLprojection X P }).prop.Lcomplement⟩⟩

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