le_succ_of_forall_lt_le — Mathlib

English

If every element z smaller than x is bounded by y, then x is bounded by the successor of y.

Русский

Если каждый элемент z, меньший чем x, удовлетворяет z ≤ y, то x ≤ succ(y).

LaTeX

$$$\forall x,y\in s,\ (\forall z\in s,\ z

Lean4

theorem le_succ_of_forall_lt_le {x y : s} (h : ∀ z < x, z ≤ y) : x ≤ succ y :=
  have hx : ∃ m, (y : ℕ) + m + 1 ∈ s := exists_succ _
  show (x : ℕ) ≤ (y : ℕ) + Nat.find hx + 1 from
    le_of_not_gt fun hxy => (h ⟨_, Nat.find_spec hx⟩ hxy).not_gt <| (by cutsat : (y : ℕ) < (y : ℕ) + Nat.find hx + 1)

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