case h.e'_3
f : Ordinal → Ordinal
H : IsNormal f
⊢ fixedPoints f = ⋂ (i : Unit), fixedPoints f
f : Ordinal → Ordinal
H : IsNormal f
⊢ Set.Unbounded (fun x x_1 => x < x_1) (fixedPoints f)
convert fp_family_unbounded fun _ : Unit => H
no goals
case h.e'_3
f : Ordinal → Ordinal
H : IsNormal f
⊢ fixedPoints f = ⋂ (i : Unit), fixedPoints f
exact (Set.iInter_const _).symm