top_mul

Mathlib.Data.ENNReal.Operations

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

English

∞ * a equals ∞ for a ≠ 0.

Русский

∞ * a = ∞ для a ≠ 0.

LaTeX

$$∀ {a : ENNReal}, ∞ * a = ∞$$

Lean4

@[simp]
theorem top_mul (h : a ≠ 0) : ∞ * a = ∞ :=
  WithTop.top_mul h

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

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

Разделы

Аффилиация

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