sub_eq_top_iff

Mathlib.Data.ENNReal.Operations

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

English

For ENNReal a, b, a − b = ∞ if and only if a = ∞ and b ≠ ∞.

Русский

Для ENNReal a, b: a − b = ∞ тогда же и только тогда, когда a = ∞ и b ≠ ∞.

LaTeX

$$$$ a - b = \infty \;\Longleftrightarrow\; a = \infty \ \land\ b \neq \infty. $$$$

Lean4

@[simp]
theorem sub_eq_top_iff : a - b = ∞ ↔ a = ∞ ∧ b ≠ ∞ :=
  WithTop.sub_eq_top_iff

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

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

Разделы

Аффилиация

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