Theorem Set.iUnion_fin_add_one_eq_iUnion_castSucc

Modification history

2026-03-24 21:53
Mathlib/Data/Fintype/Pi.lean
feat(Topology): cardinality of connected components is bounded by cardinality of fiber (#23835) …
Added Set.iUnion_fin_add_one_eq_iUnion_castSuccView on Github →