forall_lt_iff_le — Mathlib

English

Let (α, ≤) be a linearly ordered set. Then a ≤ b precisely when every element strictly below a is also strictly below b; equivalently, (for all c) if c < a then c < b holds if and only if a ≤ b.

Русский

Пусть (α, ≤) является линейно упорядоченным множеством. Тогда выполняется: a ≤ b тогда, и только тогда, что для каждого c верно c < a ⇒ c < b; эквивалентно, (∀ c) (c < a ⇒ c < b) ⇔ a ≤ b.

LaTeX

$$$ (\\\\forall c : \\alpha, c < a \\rightarrow c < b) \\Longleftrightarrow a \\le b $$$

Lean4

theorem forall_lt_iff_le : (∀ ⦃c⦄, c < a → c < b) ↔ a ≤ b :=
  ⟨le_of_forall_lt, fun h _ hca ↦ lt_of_lt_of_le hca h⟩

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