Commit 2026-02-25 00:49 450920a5

feat(SetTheory/Cardinal): generalize infinite pigeonhole principle (#34091)

1. generalize infinite_pigeonhole_card_lt and exists_infinite_fiber only to require the domain β to be infinite instead of codomain α. Also make arguments of Infinite implicit.
2. add exists_uncountable_fiber for uncountable sets.
3. fix a TODO in le_range_of_union_finset_eq_top (and also golf). PS: thanks ChatGPT for providing the informal proofs.