exists_rat_lt

Mathlib.Algebra.Order.Archimedean.Basic

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

English

Let x be any element of K; there exists a rational number q such that q.cast < x.

Русский

Пусть x ∈ K; существует рациональное q такое, что q.cast < x.

LaTeX

$$$\forall x:K,\ \exists q\in\mathbb{Q},\ q.cast < x$$$

Lean4

theorem exists_rat_lt (x : K) : ∃ q : ℚ, (q : K) < x :=
  let ⟨n, h⟩ := exists_int_lt x
  ⟨n, by rwa [Rat.cast_intCast]⟩

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

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

Разделы

Аффилиация

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