Mathlib v3 is deprecated. Go to Mathlib v4

Theorem cardinal.mk_subtype_le_of_subset

Modification history

2019-09-03 09:24
src/set_theory/cardinal.lean
feat(data/fintype): prove `card (subtype p) ≤ card α` (#1383) …
Added cardinal.mk_subtype_le_of_subsetView on Github →