instMulPosReflectLT — Mathlib

English

The bottom-extended structure inherits MulPosMono from α, i.e., a ≤ b and c ≥ 0 imply a*c ≤ b*c.

Русский

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

LaTeX

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

Lean4

instance [MulZeroClass α] [Preorder α] [MulPosReflectLT α] : MulPosReflectLT (WithBot α) where
  elim := by
    intro ⟨x, x0⟩ a b h
    simp only at h
    rcases eq_or_ne x 0 with rfl | x0'
    · simp at h
    lift x to α
    · rintro rfl
      exact (WithBot.bot_lt_coe (0 : α)).not_ge x0
    cases b
    · rw [bot_mul x0'] at h
      exact absurd h bot_le.not_gt
    cases a
    · exact WithBot.bot_lt_coe _
    simp only [← coe_mul, coe_lt_coe] at *
    norm_cast at x0
    exact lt_of_mul_lt_mul_right h x0

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