top_mul_coe_ennreal

Mathlib.Data.EReal.Operations

URI: https://scilib.ai/kg/mathlib#EReal.top_mul_coe_ennreal

English

If x ≠ 0 in ENNReal, then ⊤ · (x : EReal) = ⊤.

Русский

Если x ≠ 0 в ENNReal, то ⊤ · (x : EReal) = ⊤.

LaTeX

$$$\forall x \in \mathbb{R}_{\ge 0}^{\infty}, x \neq 0 \Rightarrow \top \cdot (x : \mathrm{EReal}) = \top$$$

Lean4

theorem top_mul_coe_ennreal {x : ℝ≥0∞} (hx : x ≠ 0) : ⊤ * (x : EReal) = ⊤ :=
  top_mul_of_pos <| coe_ennreal_pos.mpr <| pos_iff_ne_zero.mpr hx

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

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

Разделы

Аффилиация

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