toZeroLEOneClass — Mathlib

English

In a canonically ordered additive structure with 0, 1, and order, we have 0 ≤ 1.

Русский

В канонически упорядоченной аддитивной структуре с 0, 1 и порядком выполняется 0 ≤ 1.

LaTeX

$$$0 \le 1$$$

Lean4

instance (priority := 10) toZeroLEOneClass [AddZeroClass R] [One R] [LE R] [CanonicallyOrderedAdd R] : ZeroLEOneClass R
    where
  zero_le_one :=
    zero_le
      _
        -- this holds more generally if we refactor `Odd` to use
        -- either `2 • t` or `t + t` instead of `2 * t`.

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