ne_nat

Mathlib.RingTheory.Real.Irrational

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

English

If x ∈ ℝ is irrational, then x ≠ m for every m ∈ ℕ.

Русский

Пусть x ∈ ℝ иррационально. Тогда x не равно ни одному натуральному числу.

LaTeX

$$$$\forall x \in \mathbb{R}, \operatorname{Irrational}(x) \rightarrow \forall m \in \mathbb{N}, x \neq m$$$$

Lean4

theorem ne_nat (h : Irrational x) (m : ℕ) : x ≠ m :=
  h.ne_int m

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

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

Разделы

Аффилиация

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