forall_gt_imp_ge_iff_le_of_dense — Mathlib

English

In a densely ordered linear order, the condition (∀ a, a₂ < a → a₁ ≤ a) is equivalent to a₁ ≤ a₂.

Русский

В плотно упорядоченном линейном порядке условие (∀ a, a₂ < a → a₁ ≤ a) эквивалентно a₁ ≤ a₂.

LaTeX

$$$(\forall a, a_2 < a \rightarrow a_1 \le a) \iff a_1 \le a_2$$$

Lean4

theorem forall_gt_imp_ge_iff_le_of_dense : (∀ a, a₂ < a → a₁ ≤ a) ↔ a₁ ≤ a₂ :=
  ⟨le_of_forall_gt_imp_ge_of_dense, fun ha _a ha₂ ↦ ha.trans ha₂.le⟩

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