inv_eq_top

Mathlib.Data.ENNReal.Inv

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

English

inv a = ∞ if and only if a = 0.

Русский

inv a = ∞ тогда и только тогда, когда a = 0.

LaTeX

$$inv a = \infty \Leftrightarrow a = 0$$

Lean4

@[simp]
theorem inv_eq_top : a⁻¹ = ∞ ↔ a = 0 :=
  inv_zero ▸ inv_inj

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

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

Разделы

Аффилиация

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