ne_iff

Mathlib.Data.NNReal.Defs

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

English

For NNReal x,y, (x.toReal) ≠ (y.toReal) iff x ≠ y.

Русский

Для x,y ∈ ℝ≥0, (x.toReal) ≠ (y.toReal) эквивалентно x ≠ y.

LaTeX

$$$ \\forall x,y \\in \\mathbb{R}_{\\ge 0}, (x.toReal) \\neq (y.toReal) \\iff x \\neq y $$$

Lean4

theorem ne_iff {x y : ℝ≥0} : (x : ℝ) ≠ (y : ℝ) ↔ x ≠ y :=
  not_congr <| NNReal.eq_iff.symm

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

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

Разделы

Аффилиация

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