nonneg_add

Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order

URI: https://scilib.ai/kg/mathlib#IsStrictlyPositive.nonneg_add

← MathLib Explorer

English

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

Русский

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

LaTeX

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

Lean4

theorem _root_.IsStrictlyPositive.nonneg_add {a b : A} (ha : 0 ≤ a) (hb : IsStrictlyPositive b) :
    IsStrictlyPositive (a + b) :=
  add_comm a b ▸ hb.add_nonneg ha

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru