le_of_forall_gt_imp_ge_of_dense — Mathlib

English

In a densely ordered linear order, if for all a with a₂ < a we have a₁ ≤ a, then a₁ ≤ a₂.

Русский

В плотно упорядоченном линейном порядке, если для всех a, для которых a₂ < a верно a₁ ≤ a, то a₁ ≤ a₂.

LaTeX

$$$\forall {\alpha}, [\text{LinearOrder }\alpha] [\text{DenselyOrdered }\alpha]\, (\forall a, a_2 < a \Rightarrow a_1 \le a) \Rightarrow a_1 \le a_2$$$

Lean4

theorem le_of_forall_gt_imp_ge_of_dense (h : ∀ a, a₂ < a → a₁ ≤ a) : a₁ ≤ a₂ :=
  le_of_not_gt fun ha ↦
    let ⟨a, ha₁, ha₂⟩ := exists_between ha
    lt_irrefl a <| lt_of_lt_of_le ‹a < a₁› (h _ ‹a₂ < a›)

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