nnqsmul_nonneg — Mathlib

English

If q ≥ 0 and a ≥ 0, then q • a ≥ 0 in α; in particular nonnegative scalars preserve nonnegativity.

Русский

Если q ≥ 0 и a ≥ 0, то q • a ≥ 0 в α; положительные множители сохраняют неотрицательность.

LaTeX

$$$q \\ge 0 \\land a \\ge 0 \\;\Rightarrow\\; q \\cdot a \\ge 0$$$

Lean4

theorem nnqsmul_nonneg (q : ℚ≥0) (ha : 0 ≤ a) : 0 ≤ q • a := by rw [NNRat.smul_def]; exact mul_nonneg q.cast_nonneg ha

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