instMulLeftReflectLT — Mathlib

English

If f is a monotone map between α and β, then map' f is monotone on WithZero.

Русский

Если f монотонна, то map' f монотонна на WithZero.

LaTeX

$$$ \text{Monotone}(\mathrm{WithZero.map'} f) $$$

Lean4

instance instMulLeftReflectLT [Mul α] [MulLeftReflectLT α] : MulLeftReflectLT (WithZero α) :=
  by
  refine ⟨fun a b c h => ?_⟩
  have := ((zero_le _).trans_lt h).ne'
  induction a
  · simp at this
  induction c
  · simp at this
  induction b
  exacts [zero_lt_coe _, coe_lt_coe.mpr (lt_of_mul_lt_mul_left' <| coe_lt_coe.mp h)]

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