forall_lt_imp_le_iff_le_of_dense — Mathlib

English

In a dense linear order, (∀ 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_lt_imp_le_iff_le_of_dense : (∀ a < a₁, a ≤ a₂) ↔ a₁ ≤ a₂ :=
  ⟨le_of_forall_lt_imp_le_of_dense, fun ha _a ha₁ ↦ ha₁.le.trans ha⟩

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