Theorem Set.encard_ne_add_one

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.encard_ne_add_oneView on Github →