irrational_iff_ne_rational — Mathlib

English

A real number x is irrational iff it is not equal to any rational a/b with integers a,b and b ≠ 0.

Русский

Действительное число x иррационально тогда и только тогда, когда x не равно ни одной дроби a/b (целые a,b, b ≠ 0).

LaTeX

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

Lean4

theorem irrational_iff_ne_rational (x : ℝ) : Irrational x ↔ ∀ a b : ℤ, b ≠ 0 → x ≠ a / b := by
  simp [Irrational, Rat.forall, eq_comm]

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