instPosMulStrictMono — Mathlib

English

If ⊥ < a and ⊥ < b in WithBot α (with LT), then ⊥ < a*b. Positivity is preserved under multiplication of positive elements.

Русский

Если ⊥ < a и ⊥ < b в WithBot α, то ⊥ < a·b. Положительность сохраняется при умножении положительных элементов.

LaTeX

$$$\forall {a b : WithBot α}, (bot) < a \land (bot) < b \Rightarrow (bot) < a*b$$$

Lean4

instance [MulZeroClass α] [Preorder α] [PosMulStrictMono α] : PosMulStrictMono (WithBot α) where
  elim := by
    intro ⟨x, x0⟩ a b h
    simp only
    lift x to α using x0.ne_bot
    cases b
    · exact absurd h not_lt_bot
    cases a
    · simp_rw [mul_bot x0.ne.symm, ← coe_mul, bot_lt_coe]
    simp only [← coe_mul, coe_lt_coe] at *
    norm_cast at x0
    exact mul_lt_mul_of_pos_left h x0

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