eq

Mathlib.Data.NNReal.Defs

URI: https://scilib.ai/kg/mathlib#NNReal.eq

English

If two NNReal numbers have equal real values, then they are equal as NNReal numbers.

Русский

Если два NNReal имеют равные вещественные значения, то они равны как элементы NNReal.

LaTeX

$$$ \\forall n,m \\in \\mathbb{R}_{\\ge 0},\\ (n : \\mathbb{R}) = (m : \\mathbb{R}) \\Rightarrow n = m $$$

Lean4

@[ext]
protected theorem eq {n m : ℝ≥0} : (n : ℝ) = (m : ℝ) → n = m :=
  Subtype.eq

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

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

Разделы

Аффилиация

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