f : Ordinal → Ordinal
a b : Ordinal
⊢ (fun a => sup fun n => (f^[n]) a) a ≤ b ↔ ∀ (n : ℕ), (f^[n]) a ≤ b
f : Ordinal → Ordinal
a b : Ordinal
⊢ nfp f a ≤ b ↔ ∀ (n : ℕ), (f^[n]) a ≤ b
rw [← sup_iterate_eq_nfp]
no goals
f : Ordinal → Ordinal
a b : Ordinal
⊢ (fun a => sup fun n => (f^[n]) a) a ≤ b ↔ ∀ (n : ℕ), (f^[n]) a ≤ b
exact sup_le_iff