top_sub

Mathlib.Data.ENNReal.Operations

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

English

For any a ∈ ENNReal, if a ≠ ∞, then ∞ − a = ∞.

Русский

Для любого a ∈ ℝ≥0∞, если a ≠ ∞, то ∞ − a = ∞.

LaTeX

$$$$ a \neq \infty \Rightarrow \ \infty - a = \infty. $$$$

Lean4

@[simp]
theorem top_sub (ha : a ≠ ∞) : ∞ - a = ∞ := by lift a to ℝ≥0 using ha; exact top_sub_coe

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

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

Разделы

Аффилиация

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