mul_nonneg_iff_pos_imp_nonneg — Mathlib

English

Under ExistsAddOfLE, PosMulStrictMono, MulPosStrictMono, AddLeftMono, AddLeftReflectLE, we have 0 ≤ a*b iff (0 < a → 0 ≤ b) ∧ (0 < b → 0 ≤ a).

Русский

При существовании дополнения к неравенству, положительная монотонность умножения и прочие условия дают: 0 ≤ a·b эквивалентно (0<a → 0≤b) ∧ (0<b → 0≤a).

LaTeX

$$$0 \le a b \iff (0 < a \rightarrow 0 \le b) \land (0 < b \rightarrow 0 \le a)$$$

Lean4

theorem mul_nonneg_iff_pos_imp_nonneg [ExistsAddOfLE R] [PosMulStrictMono R] [MulPosStrictMono R] [AddLeftMono R]
    [AddLeftReflectLE R] : 0 ≤ a * b ↔ (0 < a → 0 ≤ b) ∧ (0 < b → 0 ≤ a) :=
  by
  refine mul_nonneg_iff.trans ?_
  simp_rw [← not_le, ← or_iff_not_imp_left]
  have := le_total a 0
  have := le_total b 0
  tauto

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