le_iff_forall_le — Mathlib

English

In a linear order, if IsSuccLimit a holds, then a ≤ b iff every c < a satisfies c ≤ b.

Русский

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

LaTeX

$$$IsSuccLimit(a) \Rightarrow (a \le b \iff \forall c < a, c \le b)$$$

Lean4

theorem le_iff_forall_le (h : IsSuccPrelimit a) : a ≤ b ↔ ∀ c < a, c ≤ b :=
  by
  use fun ha c hc ↦ hc.le.trans ha
  intro H
  by_contra! ha
  exact h b ⟨ha, fun c hb hc ↦ (H c hc).not_gt hb⟩

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