Theorem Function.Injective.encard_range

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 Function.Injective.encard_rangeView on Github →