add_ne_top

Mathlib.Data.ENNReal.Operations

URI: https://scilib.ai/kg/mathlib#ENNReal.add_ne_top

English

a + b ≠ ∞ if and only if a ≠ ∞ and b ≠ ∞.

Русский

a + b ≠ ∞ эквивалентно a ≠ ∞ и b ≠ ∞.

LaTeX

$$a + b ≠ ∞ ↔ a ≠ ∞ ∧ b ≠ ∞$$

Lean4

theorem add_ne_top : a + b ≠ ∞ ↔ a ≠ ∞ ∧ b ≠ ∞ := by simpa only [lt_top_iff_ne_top] using add_lt_top

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

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

Разделы

Аффилиация

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