toENNReal_eq_toENNReal

Mathlib.Data.EReal.Basic

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

← MathLib Explorer

English

If x,y ≥ 0 and x.toENNReal = y.toENNReal then x = y.

Русский

Если x,y ≥ 0 и x.toENNReal = y.toENNReal, то x = y.

LaTeX

$$$ x \ge 0 \land y \ge 0 \Rightarrow (x.toENNReal = y.toENNReal) \iff x = y $$$

Lean4

theorem toENNReal_eq_toENNReal {x y : EReal} (hx : 0 ≤ x) (hy : 0 ≤ y) : x.toENNReal = y.toENNReal ↔ x = y := by
  induction x <;> induction y <;> simp_all

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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