Commit 2024-11-07 18:54 185be8f6

feat: cardinalities in specific inverse systems (#18067) We compute the cardinality of each node in an inverse system F i indexed by a well-order in which every map between successive nodes has constant fiber X i, and every limit node is the limit of the inverse subsystem formed by all previous nodes. (To avoid importing Cardinal, we in fact construct a bijection rather than stating the result in terms of Cardinal.mk.)