mul_pos — Mathlib

English

If x1 and x2 are numeric and positive, then their product is positive.

Русский

Если x1 и x2 числовые и положительны, то их произведение положительно.

LaTeX

$$$$ \forall x_1\,x_2 \; (x_1.Numeric \land x_2.Numeric \land 0 < x_1 \land 0 < x_2) \Rightarrow 0 < x_1 \cdot x_2. $$$$

Lean4

theorem mul_pos (hx₁ : x₁.Numeric) (hx₂ : x₂.Numeric) (hp₁ : 0 < x₁) (hp₂ : 0 < x₂) : 0 < x₁ * x₂ :=
  by
  rw [lt_iff_game_lt]
  have := P3_of_lt_of_lt numeric_zero hx₁ numeric_zero hx₂ hp₁ hp₂
  simp_rw [P3, quot_zero_mul, quot_mul_zero, add_lt_add_iff_left] at this
  exact this

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