ne_iff

Mathlib.Data.NNRat.Defs

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

English

Two nonnegative rationals are not equal iff their casts to ℚ are not equal.

Русский

Два неотрицательных рациональных чисел не равны тогда и только тогда, когда их приведения в ℚ не равны.

LaTeX

$$$(x : \mathbb{Q}) \neq (y : \mathbb{Q}) \iff x \neq y$$$

Lean4

theorem ne_iff {x y : ℚ≥0} : (x : ℚ) ≠ (y : ℚ) ↔ x ≠ y :=
  NNRat.coe_inj.not

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

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

Разделы

Аффилиация

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