instIsOrderedRing — Mathlib

English

In an ordered ring, 0 ≤ g - f along l iff f ≤ g along l.

Русский

В упорядоченном кольце 0 ≤ g - f вдоль l эквивалентно f ≤ g вдоль l.

LaTeX

$$$ 0 \le^l (g - f) \iff f \le^l g $$$

Lean4

instance instIsOrderedRing [Semiring β] [PartialOrder β] [IsOrderedRing β] : IsOrderedRing (Germ l β)
    where
  zero_le_one := const_le zero_le_one
  mul_le_mul_of_nonneg_left x y
    z := inductionOn₃ x y z fun _f _g _h hfg hh ↦ hh.mp <| hfg.mono fun _a ↦ mul_le_mul_of_nonneg_left
  mul_le_mul_of_nonneg_right x y
    z := inductionOn₃ x y z fun _f _g _h hfg hh ↦ hh.mp <| hfg.mono fun _a ↦ mul_le_mul_of_nonneg_right

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