add_pos

Mathlib.Topology.UnitInterval

URI: https://scilib.ai/kg/mathlib#unitInterval.add_pos

English

If t ∈ I and x > 0, then 0 < x + t.

Русский

Если t ∈ I и x > 0, то 0 < x + t.

LaTeX

$$$\forall t\in I,\forall x\in \mathbb{R},\ x>0 \Rightarrow 0< x+t$$$

Lean4

theorem add_pos {t : I} {x : ℝ} (hx : 0 < x) : 0 < (x + t : ℝ) :=
  add_pos_of_pos_of_nonneg hx <| nonneg _

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

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

Разделы

Аффилиация

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