le_of_forall_lt_imp_le_of_dense — Mathlib

English

If every a < a₁ satisfies a ≤ a₂, then a₁ ≤ a₂.

Русский

Если для всех a < a₁ выполняется a ≤ a₂, то a₁ ≤ a₂.

LaTeX

$$$(\forall a < a_1)(a \le a_2) \Rightarrow a_1 \le a_2$$$

Lean4

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

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