add_lt_top

Mathlib.Data.ENat.Basic

URI: https://scilib.ai/kg/mathlib#ENat.add_lt_top

English

For a,b ∈ ℕ∞, a + b < ⊤ if and only if a < ⊤ and b < ⊤.

Русский

Для a,b ∈ ℕ∞ выполнено: a + b < ⊤ тогда и лишь тогда, когда a < ⊤ и b < ⊤.

LaTeX

$$$a+b < \\top \\iff a < \\top \\wedge b < \\top$$$

Lean4

@[simp]
theorem add_lt_top {a b : ℕ∞} : a + b < ⊤ ↔ a < ⊤ ∧ b < ⊤ :=
  WithTop.add_lt_top

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

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

Разделы

Аффилиация

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