bot_lt_mul — Mathlib

English

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

Русский

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

LaTeX

$$$\forall {a b : WithBot α}, ⊥ < a \land ⊥ < b \Rightarrow ⊥ < a*b$$$

Lean4

theorem bot_lt_mul [LT α] {a b : WithBot α} (ha : ⊥ < a) (hb : ⊥ < b) : ⊥ < a * b :=
  WithTop.mul_lt_top (α := αᵒᵈ) ha hb

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