boundedOrder — Mathlib

English

The subtype { P ∈ M | IsLprojection X P } carries a bounded order: there are bottom and top elements given by the projections 0 and 1, and each P lies between them.

Русский

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

LaTeX

$$\text{Bounded order: } \bot = 0, \top = 1, \forall P, 0 \le P \le 1.$$

Lean4

instance boundedOrder [FaithfulSMul M X] : BoundedOrder { P : M // IsLprojection X P }
    where
  top := 1
  le_top P := (mul_one (P : M)).symm
  bot := 0
  bot_le P := (zero_mul (P : M)).symm

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