ι : Type u
f : ι → Ordinal → Ordinal
i : ι
H : IsNormal (f i)
a : Ordinal
⊢ f i (sup (List.foldr f a)) = sup (List.foldr f a)
ι : Type u
f : ι → Ordinal → Ordinal
i : ι
H : IsNormal (f i)
a : Ordinal
⊢ f i (nfpFamily f a) = nfpFamily f a
unfold nfpFamily
ι : Type u
f : ι → Ordinal → Ordinal
i : ι
H : IsNormal (f i)
a : Ordinal
⊢ sup (f i ∘ List.foldr f a) = sup (List.foldr f a)
ι : Type u
f : ι → Ordinal → Ordinal
i : ι
H : IsNormal (f i)
a : Ordinal
⊢ f i (sup (List.foldr f a)) = sup (List.foldr f a)
rw [@IsNormal.sup.{u, v, v} _ H _ _ ⟨[]⟩]
case a
ι : Type u
f : ι → Ordinal → Ordinal
i : ι
H : IsNormal (f i)
a : Ordinal
l : List ι
⊢ (f i ∘ List.foldr f a) l ≤ sup (List.foldr f a)

case a
ι : Type u
f : ι → Ordinal → Ordinal
i : ι
H : IsNormal (f i)
a : Ordinal
l : List ι
⊢ List.foldr f a l ≤ sup (f i ∘ List.foldr f a)
ι : Type u
f : ι → Ordinal → Ordinal
i : ι
H : IsNormal (f i)
a : Ordinal
⊢ sup (f i ∘ List.foldr f a) = sup (List.foldr f a)
apply le_antisymm <;> refine' Ordinal.sup_le fun l => _
no goals
case a
ι : Type u
f : ι → Ordinal → Ordinal
i : ι
H : IsNormal (f i)
a : Ordinal
l : List ι
⊢ (f i ∘ List.foldr f a) l ≤ sup (List.foldr f a)
exact le_sup _ (i::l)
no goals
case a
ι : Type u
f : ι → Ordinal → Ordinal
i : ι
H : IsNormal (f i)
a : Ordinal
l : List ι
⊢ List.foldr f a l ≤ sup (f i ∘ List.foldr f a)
exact (H.self_le _).trans (le_sup _ _)