of_succ_lt — Mathlib

English

Let α be a linearly ordered type equipped with a successor operation and WellFoundedLT, and let β be a linearly ordered type. If a function f : α → β satisfies f(a) < f(succ a) for every a, and for every a that is a succ-limit we have f(a) is the least upper bound of the set { f(b) : b < a }, then f is a normal function.

Русский

Пусть α обладает линейным порядком, операцией следования succ и хорошо построенным порядком; β — линейно упорядченная. Пусть f: α → β удовлетворяет f(a) < f(succ a) для каждого a, и для каждого succ-предела a выполняется, что f(a) является наименьшей верхней гранью множества { f(b) : b < a }. Тогда f является нормальной функцией.

LaTeX

$$$\\left( \\forall a,\\ f(a) < f(\\mathrm{succ}(a)) \\right) \\wedge \\left( \\forall a, \\ \\mathrm{IsSuccLimit}(a) \\rightarrow \\mathrm{IsLUB}(f'' \\;Iio(a))\\; (f(a)) \\right) \\Rightarrow \\mathrm{IsNormal}(f).$$

Lean4

theorem of_succ_lt (hs : ∀ a, f a < f (succ a)) (hl : ∀ {a}, IsSuccLimit a → IsLUB (f '' Iio a) (f a)) : IsNormal f :=
  by
  refine ⟨fun a b ↦ ?_, fun ha ↦ (hl ha).2⟩
  induction b using SuccOrder.limitRecOn with
  | isMin b hb => exact hb.not_lt.elim
  | succ b hb IH =>
    intro hab
    obtain rfl | h := (lt_succ_iff_eq_or_lt_of_not_isMax hb).1 hab
    · exact hs a
    · exact (IH h).trans (hs b)
  | isSuccLimit b hb IH =>
    intro hab
    have hab' := hb.succ_lt hab
    exact (IH _ hab' (lt_succ_of_not_isMax hab.not_isMax)).trans_le ((hl hb).1 (mem_image_of_mem _ hab'))

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