instLeOnePart — Mathlib

English

The object representing the comparison with one (LeOnePart) is defined by a₁ ≤ a₂ if a₁ ≤ a₂ in the lattice sense, via a supremum with 1.

Русский

Инстанция LeOnePart задаёт отношение порядка через максимум с единицей в решётке.

LaTeX

$$LeOnePart α with oneLePart a := a ⊔ 1$$

Lean4

/-- The *negative part* of an element `a` in a lattice ordered group is `a⁻¹ ⊔ 1`, denoted `a⁻ᵐ `.
-/
@[to_additive /-- The *negative part* of an element `a` in a lattice ordered group is `(-a) ⊔ 0`, denoted `a⁻`.
    -/
    ]
instance instLeOnePart : LeOnePart α where leOnePart a := a⁻¹ ⊔ 1

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