exists_rat_gt

Mathlib.Algebra.Order.Archimedean.Basic

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

English

If K is Archimedean, then for every x ∈ K there exists a rational q with x < q.

Русский

Если K Архимедово упорядочено, то для каждого x ∈ K существует рациональное q, такое что x < q.

LaTeX

$$$\text{Archimedean}(K) \Rightarrow \forall x\in K,\ \exists q\in \mathbb{Q},\ x < q$$$

Lean4

theorem exists_rat_gt (x : K) : ∃ q : ℚ, x < q :=
  archimedean_iff_rat_lt.mp ‹_› _

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

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

Разделы

Аффилиация

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