Commit 2024-11-07 18:54 185be8f6
View on Github →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
.)