mathlib

c2d870e2 - feat(set_theory/{ordinal_arithmetic, fixed_points}): Next fixed point of families (#12200)

feat(set_theory/{ordinal_arithmetic, fixed_points}): Next fixed point of families (#12200) We define the next common fixed point of a family of normal ordinal functions. We prove these fixed points to be unbounded, and that their enumerator functions are normal.