English
A restatement of veblenWith_succ in simplified form for the current namespace.
Русский
Упрощённая формулировка veblenWith_succ.
LaTeX
$$veblenWith_succ (o : Ordinal) : veblenWith f (succ o) = deriv (veblenWith f o)$$
Lean4
theorem veblenWith_succ (o : Ordinal) : veblenWith f (succ o) = deriv (veblenWith f o) :=
by
rw [deriv_eq_enumOrd (hf.veblenWith o), veblenWith_of_ne_zero f (succ_ne_zero _), derivFamily_eq_enumOrd]
· apply congr_arg
ext a
rw [mem_iInter]
use fun ha ↦ ha ⟨o, lt_succ o⟩
rintro (ha : _ = _) ⟨b, hb : b < _⟩
obtain rfl | hb := lt_succ_iff_eq_or_lt.1 hb
· rw [Function.mem_fixedPoints_iff, ha]
· rw [← ha]
exact veblenWith_veblenWith_of_lt hf hb _
· exact fun o ↦ hf.veblenWith o.1
