English
Let each f_i be normal. For any ordinal a, the condition that all f_i(a) ≤ a holds if and only if there exists some o with derivFamily f o = a.
Русский
Пусть все f_i нормальны. Для любого ортрела a условие f_i(a) ≤ a для всех i эквивалентно существованию o such that derivFamily f o = a.
LaTeX
$$$$ (\forall i, f_i a \le a) \iff \exists o, derivFamily f o = a. $$$$
Lean4
theorem le_iff_derivFamily [Small.{u} ι] (H : ∀ i, IsNormal (f i)) {a} : (∀ i, f i a ≤ a) ↔ ∃ o, derivFamily f o = a :=
⟨fun ha =>
by
suffices ∀ (o), a ≤ derivFamily f o → ∃ o, derivFamily f o = a from this a (isNormal_derivFamily _).le_apply
intro o
induction o using limitRecOn with
| zero =>
intro h₁
refine ⟨0, le_antisymm ?_ h₁⟩
rw [derivFamily_zero]
exact nfpFamily_le_fp (fun i => (H i).monotone) (Ordinal.zero_le _) ha
| succ o IH =>
intro h₁
rcases le_or_gt a (derivFamily f o) with h | h
· exact IH h
refine ⟨succ o, le_antisymm ?_ h₁⟩
rw [derivFamily_succ]
exact nfpFamily_le_fp (fun i => (H i).monotone) (succ_le_of_lt h) ha
| limit o l IH =>
intro h₁
rcases eq_or_lt_of_le h₁ with h | h
· exact ⟨_, h.symm⟩
rw [derivFamily_limit _ l, ← not_le, Ordinal.iSup_le_iff, not_forall] at h
obtain ⟨o', h⟩ := h
exact IH o' o'.2 (le_of_not_ge h),
fun ⟨_, e⟩ i => e ▸ (derivFamily_fp (H i) _).le⟩
