Commit 2023-01-16 17:55 8b8d89a7

View on Github →

feat: port Data.Fintype.Basic (#1593)

Estimated changes

Modified Mathlib/Data/Finset/Basic.lean

Modified Mathlib/Data/Fintype/Basic.lean

added theorem Fin.image_castSucc

added theorem Fin.image_succAbove_univ

added theorem Fin.image_succ_univ

added theorem Fin.univ_castSucc

added theorem Fin.univ_def

added theorem Fin.univ_succ

added theorem Fin.univ_succAbove

added theorem Finset.Nonempty.eq_univ

added theorem Finset.attach_eq_univ

added theorem Finset.codisjoint_left

added theorem Finset.codisjoint_right

added theorem Finset.coe_compl

added theorem Finset.coe_eq_univ

added theorem Finset.coe_filter_univ

added theorem Finset.coe_univ

added theorem Finset.compl_empty

added theorem Finset.compl_eq_empty_iff

added theorem Finset.compl_eq_univ_iff

added theorem Finset.compl_eq_univ_sdiff

added theorem Finset.compl_erase

added theorem Finset.compl_filter

added theorem Finset.compl_insert

added theorem Finset.compl_inter

added theorem Finset.compl_ne_univ_iff_nonempty

added theorem Finset.compl_singleton

added theorem Finset.compl_union

added theorem Finset.compl_univ

added theorem Finset.eq_univ_iff_forall

added theorem Finset.eq_univ_of_forall

added theorem Finset.image_univ_of_surjective

added theorem Finset.insert_compl_self

added theorem Finset.insert_inj_on'

added theorem Finset.inter_compl

added theorem Finset.inter_univ

added theorem Finset.map_univ_equiv

added theorem Finset.map_univ_of_surjective

added theorem Finset.mem_compl

modified theorem Finset.mem_univ

added theorem Finset.mem_univ_val

added theorem Finset.not_mem_compl

added theorem Finset.piecewise_compl

added theorem Finset.piecewise_erase_univ

added theorem Finset.piecewise_univ

added theorem Finset.sdiff_eq_inter_compl

added theorem Finset.ssubset_univ_iff

added theorem Finset.subset_univ

added theorem Finset.toFinset_coe

added theorem Finset.top_eq_univ

added theorem Finset.union_compl

modified def Finset.univ

added theorem Finset.univ_eq_attach

added theorem Finset.univ_eq_empty

added theorem Finset.univ_eq_empty_iff

added theorem Finset.univ_filter_exists

added theorem Finset.univ_filter_mem_range

added theorem Finset.univ_inter

added theorem Finset.univ_map_equiv_to_embedding

added theorem Finset.univ_nonempty

added theorem Finset.univ_nonempty_iff

added theorem Finset.univ_unique

added def Fintype.bijInv

added theorem Fintype.bijective_bijInv

added def Fintype.choose

added def Fintype.chooseX

added theorem Fintype.choose_spec

added theorem Fintype.choose_subtype_eq

added theorem Fintype.coe_image_univ

added theorem Fintype.finsetEquivSet_apply

added theorem Fintype.finsetEquivSet_symm_apply

added theorem Fintype.leftInverse_bijInv

added def Fintype.ofBijective

added def Fintype.ofEquiv

added def Fintype.ofFinset

added def Fintype.ofList

added def Fintype.ofMultiset

added def Fintype.ofSubsingleton

added def Fintype.ofSurjective

added def Fintype.prodLeft

added def Fintype.prodRight

added theorem Fintype.rightInverse_bijInv

added theorem Fintype.univ_Prop

added theorem Fintype.univ_bool

added theorem Fintype.univ_empty

added theorem Fintype.univ_ofSubsingleton

added theorem Fintype.univ_of_isEmpty

added theorem Fintype.univ_pempty

added theorem Fintype.univ_punit

added theorem Fintype.univ_unit

added theorem Function.Embedding.invFun_restrict

added def Function.Embedding.invOfMemRange

added theorem Function.Embedding.invOfMemRange_surjective

added theorem Function.Embedding.left_inv_of_invOfMemRange

added theorem Function.Embedding.right_inv_of_invOfMemRange

added theorem Function.Injective.invFun_restrict

added def Function.Injective.invOfMemRange

added theorem Function.Injective.invOfMemRange_surjective

added theorem Function.Injective.left_inv_of_invOfMemRange

added theorem Function.Injective.right_inv_of_invOfMemRange

added theorem Multiset.count_univ

added def Quotient.finChoice

added def Quotient.finChoiceAux'

added theorem Quotient.finChoiceAux'_eq

added def Quotient.finChoiceAux

added theorem Quotient.finChoiceAux_eq

added theorem Quotient.finChoice_eq

added theorem Set.coe_toFinset

added def Set.decidableMemOfFintype

added theorem Set.disjoint_toFinset

added theorem Set.filter_mem_univ_eq_toFinset

added theorem Set.mem_toFinset

added theorem Set.ssubset_toFinset

added theorem Set.subset_toFinset

added def Set.toFinset

added theorem Set.toFinset_compl

added theorem Set.toFinset_congr

added theorem Set.toFinset_diff

added theorem Set.toFinset_empty

added theorem Set.toFinset_eq_empty

added theorem Set.toFinset_eq_univ

added theorem Set.toFinset_image

added theorem Set.toFinset_inj

added theorem Set.toFinset_insert

added theorem Set.toFinset_inter

added theorem Set.toFinset_nonempty

added theorem Set.toFinset_ofFinset

added theorem Set.toFinset_range

added theorem Set.toFinset_singleton

added theorem Set.toFinset_ssubset

added theorem Set.toFinset_ssubset_toFinset

added theorem Set.toFinset_ssubset_univ

added theorem Set.toFinset_subset

added theorem Set.toFinset_subset_toFinset

added theorem Set.toFinset_symmDiff

added theorem Set.toFinset_union

added theorem Set.toFinset_univ

added theorem Set.to_finset_set_of

added def Unique.fintype

added theorem exists_seq_of_forall_finset_exists'

added theorem exists_seq_of_forall_finset_exists

added theorem mem_image_univ_iff_mem_range

added def setFintype

added def truncOfMultisetExistsMem

added def truncOfNonemptyFintype

added def truncSigmaOfExists

added def unitsEquivNeZero

added def unitsEquivProdSubtype

Modified Mathlib/Logic/Basic.lean

added theorem eqRec_heq'