coe_ennreal_mul_top

Mathlib.Data.EReal.Operations

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

English

For x ∈ ENNReal, if x ≠ 0 then (x : EReal) * ⊤ = ⊤.

Русский

Для x ∈ ENNReal, если x ≠ 0, тогда (x : EReal) * ⊤ = ⊤.

LaTeX

$$$\forall x \in \mathrm{ENNReal}, x \neq 0 \Rightarrow (x : \mathrm{EReal}) \cdot \top = \top$$$

Lean4

theorem coe_ennreal_mul_top {x : ℝ≥0∞} (hx : x ≠ 0) : (x : EReal) * ⊤ = ⊤ := by
  rw [EReal.mul_comm, top_mul_coe_ennreal hx]

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

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

Разделы

Аффилиация

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