ne_rational

Mathlib.RingTheory.Real.Irrational

URI: https://scilib.ai/kg/mathlib#Irrational.ne_rational

English

If x is irrational, then x is not equal to any rational a/b.

Русский

Если x иррационально, то x не равно ни одной дроби a/b с a,b ∈ ℤ и b ≠ 0.

LaTeX

$$$Irrational(x) \Rightarrow \forall a,b \in \mathbb{Z}, b \neq 0 \rightarrow x \neq \frac{a}{b}$$$

Lean4

theorem ne_rational {x : ℝ} (hx : Irrational x) (a b : ℤ) : x ≠ a / b := by rintro rfl; exact hx ⟨a / b, by simp⟩

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

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

Разделы

Аффилиация

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