le_of_forall_rat_lt_imp_le — Mathlib

English

If every rational q with q < x also satisfies q ≤ y, then x ≤ y.

Русский

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

LaTeX

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

Lean4

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

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