add_nonneg — Mathlib

English

If a is strictly positive and b ≥ 0, then a + b is strictly positive.

Русский

Если a строго положительно, и b ≥ 0, то a + b строго положительно.

LaTeX

$$ha : IsStrictlyPositive a, hb : 0 ≤ b \\Rightarrow IsStrictlyPositive (a + b)$$

Lean4

theorem _root_.IsStrictlyPositive.add_nonneg {a b : A} (ha : IsStrictlyPositive a) (hb : 0 ≤ b) :
    IsStrictlyPositive (a + b) :=
  IsStrictlyPositive.of_le ha ((le_add_iff_nonneg_right a).mpr hb)

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