isStrictlyPositive_add — Mathlib

English

Let A be a partially ordered star-ordered ring. If either a is strictly positive and b is nonnegative, or a is nonnegative and b is strictly positive, then a + b is strictly positive.

Русский

Пусть A — частично упорядочённое звёздно упорядоченное кольцо. Если либо a ∈ A строго положительно и b ≥ 0, либо a ≥ 0 и b строго положительно, тогда a + b строго положительно.

LaTeX

$$$\\big((\\mathrm{IsStrictlyPositive}(a) \\wedge 0 \\le b) \\lor (0 \\le a \\wedge \\mathrm{IsStrictlyPositive}(b))\\big) \\Rightarrow \\mathrm{IsStrictlyPositive}(a+b).$$$

Lean4

@[grind ←, aesop 90% apply]
theorem _root_.isStrictlyPositive_add {a b : A} (h : IsStrictlyPositive a ∧ 0 ≤ b ∨ 0 ≤ a ∧ IsStrictlyPositive b) :
    IsStrictlyPositive (a + b) := by grind [IsStrictlyPositive.add_nonneg, IsStrictlyPositive.nonneg_add]

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