Theorem Set.exists_ne_map_eq_of_encard_lt_of_maps_to

Modification history

2025-08-03 21:39
Mathlib/Data/Set/Card.lean
feat: a finite union of proper submodules is a proper subset (#27598) …
Added Set.exists_ne_map_eq_of_encard_lt_of_maps_toView on Github →