forall_gt_iff_le — Mathlib

English

In a linearly ordered set, the statement (for all c, a < c → b < c) is equivalent to b ≤ a.

Русский

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

LaTeX

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

Lean4

theorem forall_gt_iff_le : (∀ ⦃c⦄, a < c → b < c) ↔ b ≤ a :=
  ⟨le_of_forall_gt, fun h _ hac ↦ lt_of_le_of_lt h hac⟩

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