top_div

Mathlib.Data.ENNReal.Inv

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

English

The quotient $\infty / a$ is given by a piecewise rule: it equals 0 if a = ∞, and ∞ otherwise.

Русский

Частное \infty / a задаётся по следующему правилу: если a = ∞, то 0, иначе — ∞.

LaTeX

$$$\dfrac{\infty}{a} = \begin{cases}0, & a=\infty \\\infty, & a\neq \infty\end{cases}$$$

Lean4

theorem top_div : ∞ / a = if a = ∞ then 0 else ∞ := by simp [div_eq_mul_inv, top_mul']

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

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

Разделы

Аффилиация

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