Commit 2022-04-10 01:48 c2d870e2

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.