ι : Type u
f✝ : ι → Ordinal → Ordinal
f : ι → Ordinal → Ordinal
o : Ordinal
⊢ succ (derivFamily f o) ≤ nfpFamily f (succ (derivFamily f o))
ι : Type u
f✝ : ι → Ordinal → Ordinal
f : ι → Ordinal → Ordinal
o : Ordinal
⊢ derivFamily f o < derivFamily f (succ o)
rw [derivFamily_succ, ← succ_le_iff]
no goals
ι : Type u
f✝ : ι → Ordinal → Ordinal
f : ι → Ordinal → Ordinal
o : Ordinal
⊢ succ (derivFamily f o) ≤ nfpFamily f (succ (derivFamily f o))
apply le_nfpFamily
no goals
ι : Type u
f✝ : ι → Ordinal → Ordinal
f : ι → Ordinal → Ordinal
o : Ordinal
l : IsLimit o
a : Ordinal
⊢ derivFamily f o ≤ a ↔ ∀ (b : Ordinal), b < o → derivFamily f b ≤ a
rw [derivFamily_limit _ l, bsup_le_iff]