instOneLePart — Mathlib

English

The negative part a⁻ᵐ is defined as a⁻¹ ⊔ 1 in a lattice ordered group.

Русский

Отрицательная часть a⁻ᵐ определяется как a⁻¹ ⊔ 1 в решётке упорядоченной группы.

LaTeX

$$$a^{-\!\mathrm{m}} = a^{-1} \vee 1$$$

Lean4

/-- The *positive part* of an element `a` in a lattice ordered group is `a ⊔ 1`, denoted `a⁺ᵐ`. -/
@[to_additive /-- The *positive part* of an element `a` in a lattice ordered group is `a ⊔ 0`, denoted `a⁺`. -/
    ]
instance instOneLePart : OneLePart α where oneLePart a := a ⊔ 1

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