le_of_forall_lt_rat_imp_le

Mathlib.Algebra.Order.Archimedean.Basic

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

← MathLib Explorer

English

If every rational q with y < q has q ≤ x, then x ≥ y.

Русский

Если для каждого рационального q с y < q выполняется q ≤ x, то x ≥ y.

LaTeX

$$$\big(\forall q\in\mathbb{Q},\ y < q \Rightarrow q \le x\big) \Rightarrow x \ge y$$$

Lean4

theorem le_of_forall_lt_rat_imp_le (h : ∀ q : ℚ, y < q → x ≤ q) : x ≤ y :=
  le_of_not_gt fun hyx =>
    let ⟨_, hy, hx⟩ := exists_rat_btwn hyx
    hx.not_ge <| h _ hy

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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