not_irrational

Mathlib.RingTheory.Real.Irrational

URI: https://scilib.ai/kg/mathlib#Rat.not_irrational

English

Every rational number is not irrational.

Русский

Каждое рациональное число рационально, следовательно, не иррационально.

LaTeX

$$$$\forall q \in \mathbb{Q}, \neg \operatorname{Irrational}(q)$$$$

Lean4

@[simp]
theorem not_irrational (q : ℚ) : ¬Irrational q := fun h => h ⟨q, rfl⟩

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

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

Разделы

Аффилиация

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