Commit 2023-01-19 11:44 cd8f5ab3

View on Github →

feat: port Data.Fintype.Card (#1668)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Data/Fintype/Card.lean

added def Equiv.ofLeftInverseOfCardLe

added def Equiv.ofRightInverseOfCardLe

added theorem Fin.cast_eq_cast'

added theorem Fin.equiv_iff_eq

added theorem Finite.Preorder.wellFounded_gt

added theorem Finite.Preorder.wellFounded_lt

added theorem Finite.exists_infinite_fiber

added theorem Finite.exists_ne_map_eq_of_infinite

added theorem Finite.exists_univ_list

added theorem Finite.injective_iff_bijective

added theorem Finite.injective_iff_surjective

added theorem Finite.injective_iff_surjective_of_equiv

added theorem Finite.of_injective

added theorem Finite.of_surjective

added theorem Finite.surjective_iff_bijective

added theorem Finite.surjective_of_injective

added theorem Finite.wellFounded_of_trans_of_irrefl

added theorem Finset.card_compl

added theorem Finset.card_compl_lt_iff_nonempty

added theorem Finset.card_eq_iff_eq_univ

added theorem Finset.card_fin

added theorem Finset.card_le_univ

added theorem Finset.card_lt_iff_ne_univ

added theorem Finset.card_lt_univ_of_not_mem

added theorem Finset.card_univ

added theorem Finset.card_univ_diff

added theorem Finset.eq_univ_of_card

added theorem Finset.exists_maximal

added theorem Finset.exists_minimal

added theorem Finset.univ_map_embedding

added theorem Fintype.bijective_iff_injective_and_card

added theorem Fintype.bijective_iff_surjective_and_card

added def Fintype.card

added def Fintype.cardEqZeroEquivEquivEmpty

added theorem Fintype.card_Prop

added theorem Fintype.card_bool

added theorem Fintype.card_coe

added theorem Fintype.card_compl_eq_card_compl

added theorem Fintype.card_compl_set

added theorem Fintype.card_congr'

added theorem Fintype.card_congr

added theorem Fintype.card_empty

added theorem Fintype.card_eq

added theorem Fintype.card_eq_one_iff

added theorem Fintype.card_eq_one_iff_nonempty_unique

added theorem Fintype.card_eq_one_of_forall_eq

added theorem Fintype.card_eq_zero

added theorem Fintype.card_eq_zero_iff

added theorem Fintype.card_fin

added theorem Fintype.card_le_of_embedding

added theorem Fintype.card_le_of_injective

added theorem Fintype.card_le_of_surjective

added theorem Fintype.card_le_one_iff

added theorem Fintype.card_le_one_iff_subsingleton

added theorem Fintype.card_lex

added theorem Fintype.card_lt_of_injective_not_surjective

added theorem Fintype.card_lt_of_injective_of_not_mem

added theorem Fintype.card_lt_of_surjective_not_injective

added theorem Fintype.card_ne_zero

added theorem Fintype.card_of_bijective

added theorem Fintype.card_of_finset'

added theorem Fintype.card_of_finset

added theorem Fintype.card_of_is_empty

added theorem Fintype.card_of_subsingleton

added theorem Fintype.card_of_subtype

added theorem Fintype.card_order_dual

added theorem Fintype.card_pempty

added theorem Fintype.card_plift

added theorem Fintype.card_pos

added theorem Fintype.card_pos_iff

added theorem Fintype.card_punit

added theorem Fintype.card_quotient_le

added theorem Fintype.card_quotient_lt

added theorem Fintype.card_range

added theorem Fintype.card_range_le

added theorem Fintype.card_subtype

added theorem Fintype.card_subtype_compl

added theorem Fintype.card_subtype_eq'

added theorem Fintype.card_subtype_eq

added theorem Fintype.card_subtype_le

added theorem Fintype.card_subtype_lt

added theorem Fintype.card_subtype_mono

added theorem Fintype.card_ulift

added theorem Fintype.card_unique

added theorem Fintype.card_unit

added theorem Fintype.exists_ne_map_eq_of_card_lt

added theorem Fintype.exists_ne_of_one_lt_card

added theorem Fintype.exists_pair_of_one_lt_card

added theorem Fintype.induction_subsingleton_or_nontrivial

added theorem Fintype.ofEquiv_card

added theorem Fintype.one_lt_card

added theorem Fintype.one_lt_card_iff

added theorem Fintype.one_lt_card_iff_nontrivial

added theorem Fintype.subtype_card

added def Fintype.truncEquivFin

added def Fintype.truncEquivFinOfCardEq

added def Fintype.truncEquivOfCardEq

added def Fintype.truncFinBijection

added theorem Function.Embedding.equiv_of_fintype_self_embedding_to_embedding

added theorem Function.Embedding.exists_of_card_le_finset

added theorem Function.Embedding.is_empty_of_card_lt

added theorem Function.Embedding.nonempty_iff_card_le

added theorem Function.Embedding.nonempty_of_card_le

added def Function.Embedding.truncOfCardLe

added theorem Function.LeftInverse.rightInverse_of_card_le

added theorem Function.RightInverse.leftInverse_of_card_le

added theorem Infinite.exists_not_mem_finset

added theorem Infinite.exists_subset_card_eq

added theorem Infinite.exists_superset_card_eq

added theorem Infinite.of_injective

added theorem Infinite.of_injective_to_set

added theorem Infinite.of_not_fintype

added theorem Infinite.of_surjective

added theorem Infinite.of_surjective_from_set

added theorem List.Nodup.length_le_card

added theorem Set.toFinset_card

added theorem card_finset_fin_le

added theorem fin_injective

added theorem finite_iff_nonempty_fintype

added theorem is_empty_fintype

added theorem nonempty_fintype

added theorem not_injective_infinite_finite

added theorem not_surjective_finite_infinite

added theorem set_fintype_card_eq_univ_iff

added theorem set_fintype_card_le_univ

added def truncOfCardPos

added theorem univ_eq_singleton_of_card_one