instPosMulReflectLE — Mathlib

English

WithBot α inherits MulPosReflectLT: if a < b and c > 0, then a*c < b*c.

Русский

Расширение снизу наследует MulPosReflectLT: если a < b и c > 0, то a·c < b·c.

LaTeX

$$$\forall {a,b,c : WithBot α}, a < b \land c > 0 \Rightarrow a*c < b*c$$$

Lean4

instance [MulZeroClass α] [Preorder α] [PosMulReflectLE α] : PosMulReflectLE (WithBot α) where
  elim := by
    intro ⟨x, x0⟩ a b h
    simp only at h
    lift x to α using x0.ne_bot
    cases a
    · exact bot_le
    cases b
    · rw [mul_bot x0.ne.symm, ← coe_mul] at h
      exact absurd h (bot_lt_coe _).not_ge
    simp only [← coe_mul, coe_le_coe] at *
    norm_cast at x0
    exact le_of_mul_le_mul_left h x0

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