ofReal_toReal_eq_iff

Mathlib.Data.ENNReal.Basic

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

English

For any ENNReal x, x.toNNReal = 1 iff x = 1.

Русский

Для любого ENNReal x, x.toNNReal = 1 эквивалентно x = 1.

LaTeX

$$$$ x.toNNReal = 1 \iff x = 1. $$$$

Lean4

@[simp]
theorem ofReal_toReal_eq_iff : ENNReal.ofReal a.toReal = a ↔ a ≠ ⊤ :=
  ⟨fun h => by
    rw [← h]
    exact ofReal_ne_top, ofReal_toReal⟩

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

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

Разделы

Аффилиация

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