instMulPosReflectLE — Mathlib

English

WithBot α inherits MulPosReflectLE: if a ≤ b and c ≥ 0, then a*c ≤ b*c.

Русский

Расширение снизу наследует MulPosReflectLE: если a ≤ b и c ≥ 0, то a·c ≤ b·c.

LaTeX

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

Lean4

instance [MulZeroClass α] [Preorder α] [MulPosReflectLE α] : MulPosReflectLE (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 [bot_mul 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_right h x0

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