Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-06-10 05:26 e3dade35

View on Github →

feat(data/finite/basic): finite predicate (#14373) Introduces a Prop-valued finiteness predicate on types and adapts some subset of the fintype API to get started. Uses nat.card as the primary cardinality function.

Estimated changes

added theorem equiv.finite_iff
added theorem finite.card_eq
added theorem finite.card_option
added theorem finite.card_pos_iff
added theorem finite.card_subtype_le
added theorem finite.card_subtype_lt
added theorem finite.card_sum
added def finite.equiv_fin
added theorem finite.exists_max
added theorem finite.exists_min
added theorem finite.of_bijective
added theorem finite.of_equiv
added theorem finite.of_fintype
added theorem finite.of_injective
added theorem finite.of_not_infinite
added theorem finite.of_surjective
added theorem finite.one_lt_card
added theorem finite.prod_left
added theorem finite.prod_right
added theorem finite.sum_left
added theorem finite.sum_right
added theorem finite_or_infinite
added theorem infinite.of_not_finite
added theorem nat.card_eq
added theorem not_finite
added theorem of_subsingleton
added theorem nat.card_congr
added theorem nat.card_of_is_empty
added theorem nat.card_plift
added theorem nat.card_prod
added theorem nat.card_ulift
added theorem nat.card_unique