Irrational

Mathlib.RingTheory.Real.Irrational

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

English

A real number is irrational if it is not equal to any rational number.

Русский

Действительное число иррационально, если оно не равно ни одному рациональному числу.

LaTeX

$$$Irrational(x) \iff x \notin \mathbb{Q}$$$

Lean4

/-- A real number is irrational if it is not equal to any rational number. -/
def Irrational (x : ℝ) :=
  x ∉ Set.range ((↑) : ℚ → ℝ)

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

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

Разделы

Аффилиация

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