toOrderBot — Mathlib

English

Every IdemSemiring α carries an OrderBot structure, with the order defined by a ≤ b iff a + b = b and bottom element 0.

Русский

У любого IdemSemiring α существует структура OrderBot, где порядок задаётся как a ≤ b ⇔ a + b = b, а нижняя граница равна 0.

LaTeX

$$$ a \le b \iff a + b = b \quad\text{and}\quad \bot = 0 $$$

Lean4

instance (priority := 100) toOrderBot [IdemSemiring α] : OrderBot α :=
  { ‹IdemSemiring α› with }
    -- See note [reducible non-instances]

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