top_mul'

Mathlib.Data.ENNReal.Operations

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

English

∞ * a equals a finite expression depending on a; specifically, if a = 0 then 0 else ∞.

Русский

∞ * a равно выражению, зависящему от a: если a = 0, то 0, иначе ∞.

LaTeX

$$top_mul' (a := a)$$

Lean4

theorem top_mul' : ∞ * a = if a = 0 then 0 else ∞ := by convert WithTop.top_mul' a

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

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

Разделы

Аффилиация

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