enumOrd_succ_le — Mathlib

English

If s is not bounded above, and a ∈ s, and enumOrd(s, b) < a, then enumOrd(s, succ(b)) ≤ a.

Русский

Если s не ограничено сверху, и a ∈ s, и enumOrd(s, b) < a, тогда enumOrd(s, succ(b)) ≤ a.

LaTeX

$$$\forall s : \mathrm{Set}\ \mathrm{Ordinal},\, \neg \mathrm{BddAbove}(s) \Rightarrow \forall a \in s, \forall b : \mathrm{Ordinal},\, \mathrm{enumOrd}(s,b) < a \Rightarrow \mathrm{enumOrd}(s,\mathrm{succ}(b)) \le a$$$

Lean4

theorem enumOrd_succ_le (hs : ¬BddAbove s) (ha : a ∈ s) (hb : enumOrd s b < a) : enumOrd s (succ b) ≤ a :=
  by
  apply enumOrd_le_of_forall_lt ha
  intro c hc
  rw [lt_succ_iff] at hc
  exact ((enumOrd_strictMono hs).monotone hc).trans_lt hb

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