instNoMaxOrderSubtypeReal

Mathlib.Topology.Instances.Irrational

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

English

There is no maximal irrational number under the usual order.

Русский

У множества иррациональных чисел нет максимального элемента по обычному порядку.

LaTeX

$$$\text{NoMaxOrder}(\{x \in \mathbb{R} \mid \operatorname{Irrational}(x)\})$$$

Lean4

instance : NoMaxOrder { x // Irrational x } :=
  ⟨fun ⟨x, hx⟩ => ⟨⟨x + (1 : ℕ), hx.add_natCast 1⟩, by simp⟩⟩

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

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

Разделы

Аффилиация

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