le_of_forall_gt — Mathlib

English

Let α be a linearly ordered set and a, b ∈ α. If for every c we have a < c implies b < c, then b ≤ a.

Русский

Пусть α — линейный упорядоченный множество и a, b ∈ α. Если для каждого c верно a < c ⇒ b < c, то b ≤ a.

LaTeX

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

Lean4

theorem le_of_forall_gt (H : ∀ c, a < c → b < c) : b ≤ a :=
  le_of_not_gt fun h ↦ lt_irrefl _ (H _ h)

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