Theorem Set.ncard_le_encard

Modification history

2026-07-17 11:15
Mathlib/Data/Set/Card.lean
chore(Data/ENat): replace `coe` with `natCast` in lemma names (#41140) …
Modified Set.ncard_le_encardView on Github →
2025-02-06 20:37
Mathlib/Data/Set/Card.lean
feat(Data/Set/Card): add `ncard_le_encard` (#21467)
Added Set.ncard_le_encardView on Github →