Commit 2025-02-17 17:27 9d1a5226

View on Github →

chore(Data/Fintype): split Data/Fintype/Basic.lean (#21831) This PR splits Data.Fintype.Basic into the following files:

Data.Fintype.Defs: definition of Fintype and Finset.univ
Data.Finset.BooleanAlgebra: shows Finset is a boolean algebra (with Finset.univ as top element)
Data.Fintype.Basic: instances for Fintype on most basic types such as products and pi types
Data.Fintype.Group: finiteness and additive/multiplicative structures
Data.Fintype.Inv: computably choosing existential witnesses and constructing inverse functions
Data.Fintype.OfMap: constructors for Fintype given maps from/to finite types
Data.Fintype.Sets: equivalence between Set and Finset on finite types A particular goal is to avoid importing the algebra hierarchy while working on finiteness and eventually into measure theory.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/BigOperators/Group/Finset/Defs.lean

Modified Mathlib/Algebra/Divisibility/Finite.lean

Created Mathlib/Algebra/Group/TypeTags/Fintype.lean

Modified Mathlib/Algebra/Order/Field/Pi.lean

Modified Mathlib/Computability/PostTuringMachine.lean

Modified Mathlib/Control/EquivFunctor/Instances.lean

Modified Mathlib/Data/Fin/Fin2.lean

Created Mathlib/Data/Finset/BooleanAlgebra.lean

added theorem Finset.Nonempty.eq_univ

added theorem Finset.codisjoint_left

added theorem Finset.codisjoint_right

added theorem Finset.coe_compl

added theorem Finset.coe_filter_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_ssubset_compl

added theorem Finset.compl_subset_compl

added theorem Finset.compl_union

added theorem Finset.compl_univ

added theorem Finset.filter_univ_mem

added theorem Finset.image_univ_equiv

added theorem Finset.image_univ_of_surjective

added theorem Finset.insert_compl_insert

added theorem Finset.insert_compl_self

added theorem Finset.insert_inj_on'

added theorem Finset.inter_compl

added theorem Finset.inter_eq_univ

added theorem Finset.inter_univ

added theorem Finset.map_univ_equiv

added theorem Finset.map_univ_of_surjective

added theorem Finset.mem_compl

added theorem Finset.not_mem_compl

added theorem Finset.sdiff_eq_inter_compl

added theorem Finset.singleton_eq_univ

added theorem Finset.ssubset_univ_iff

added theorem Finset.subset_compl_comm

added theorem Finset.subset_compl_singleton

added theorem Finset.subtype_eq_univ

added theorem Finset.subtype_univ

added theorem Finset.top_eq_univ

added theorem Finset.union_compl

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_map_subtype

added theorem Finset.univ_nonempty

added theorem Finset.univ_nonempty_iff

added theorem Finset.univ_nontrivial

added theorem Finset.univ_nontrivial_iff

added theorem Finset.univ_subset_iff

added theorem Finset.univ_unique

added theorem Finset.univ_val_map_subtype_restrict

added theorem Finset.univ_val_map_subtype_val

Modified Mathlib/Data/Finset/Image.lean

Modified Mathlib/Data/Finset/Piecewise.lean

Modified Mathlib/Data/Fintype/Basic.lean

deleted theorem Finset.Nonempty.eq_univ

deleted theorem Finset.attach_eq_univ

deleted theorem Finset.codisjoint_left

deleted theorem Finset.codisjoint_right

deleted theorem Finset.coe_compl

deleted theorem Finset.coe_eq_univ

deleted theorem Finset.coe_filter_univ

deleted theorem Finset.coe_univ

deleted theorem Finset.compl_empty

deleted theorem Finset.compl_eq_empty_iff

deleted theorem Finset.compl_eq_univ_iff

deleted theorem Finset.compl_eq_univ_sdiff

deleted theorem Finset.compl_erase

deleted theorem Finset.compl_filter

deleted theorem Finset.compl_insert

deleted theorem Finset.compl_inter

deleted theorem Finset.compl_ne_univ_iff_nonempty

deleted theorem Finset.compl_singleton

deleted theorem Finset.compl_ssubset_compl

deleted theorem Finset.compl_subset_compl

deleted theorem Finset.compl_union

deleted theorem Finset.compl_univ

deleted theorem Finset.eq_univ_iff_forall

deleted theorem Finset.eq_univ_of_forall

deleted theorem Finset.filter_univ_mem

deleted theorem Finset.image_univ_equiv

deleted theorem Finset.image_univ_of_surjective

deleted theorem Finset.insert_compl_insert

deleted theorem Finset.insert_compl_self

deleted theorem Finset.insert_inj_on'

deleted theorem Finset.inter_compl

deleted theorem Finset.inter_eq_univ

deleted theorem Finset.inter_univ

deleted theorem Finset.map_univ_equiv

deleted theorem Finset.map_univ_of_surjective

deleted theorem Finset.mem_compl

deleted theorem Finset.mem_univ

deleted theorem Finset.mem_univ_val

deleted theorem Finset.not_mem_compl

deleted theorem Finset.sdiff_eq_inter_compl

deleted theorem Finset.singleton_eq_univ

deleted theorem Finset.ssubset_univ_iff

deleted theorem Finset.subset_compl_comm

deleted theorem Finset.subset_compl_singleton

deleted theorem Finset.subset_univ

deleted theorem Finset.subtype_eq_univ

deleted theorem Finset.subtype_univ

deleted theorem Finset.toFinset_coe

deleted theorem Finset.top_eq_univ

deleted theorem Finset.union_compl

deleted def Finset.univ

deleted theorem Finset.univ_eq_attach

deleted theorem Finset.univ_eq_empty

deleted theorem Finset.univ_eq_empty_iff

deleted theorem Finset.univ_filter_exists

deleted theorem Finset.univ_filter_mem_range

deleted theorem Finset.univ_inter

deleted theorem Finset.univ_map_equiv_to_embedding

deleted theorem Finset.univ_map_subtype

deleted theorem Finset.univ_nonempty

deleted theorem Finset.univ_nonempty_iff

deleted theorem Finset.univ_nontrivial

deleted theorem Finset.univ_nontrivial_iff

deleted theorem Finset.univ_subset_iff

deleted theorem Finset.univ_unique

deleted theorem Finset.univ_val_map_subtype_restrict

deleted theorem Finset.univ_val_map_subtype_val

deleted def Fintype.bijInv

deleted theorem Fintype.bijective_bijInv

deleted def Fintype.choose

deleted def Fintype.chooseX

deleted theorem Fintype.choose_spec

deleted theorem Fintype.choose_subtype_eq

deleted theorem Fintype.coe_finsetEquivSet

deleted theorem Fintype.coe_finsetOrderIsoSet

deleted theorem Fintype.coe_finsetOrderIsoSet_symm

deleted theorem Fintype.coe_image_univ

deleted theorem Fintype.finsetEquivSet_apply

deleted theorem Fintype.finsetEquivSet_symm_apply

deleted theorem Fintype.leftInverse_bijInv

deleted def Fintype.ofBijective

deleted def Fintype.ofEquiv

deleted def Fintype.ofFinset

deleted def Fintype.ofIsEmpty

deleted def Fintype.ofList

deleted def Fintype.ofMultiset

deleted def Fintype.ofSubsingleton

deleted def Fintype.ofSurjective

deleted theorem Fintype.rightInverse_bijInv

deleted theorem Fintype.univ_Prop

deleted theorem Fintype.univ_ofIsEmpty

deleted theorem Fintype.univ_ofSubsingleton

deleted theorem Function.Embedding.invFun_restrict

deleted def Function.Embedding.invOfMemRange

deleted theorem Function.Embedding.invOfMemRange_surjective

deleted theorem Function.Embedding.left_inv_of_invOfMemRange

deleted theorem Function.Embedding.right_inv_of_invOfMemRange

deleted theorem Function.Injective.invFun_restrict

deleted def Function.Injective.invOfMemRange

deleted theorem Function.Injective.invOfMemRange_surjective

deleted theorem Function.Injective.left_inv_of_invOfMemRange

deleted theorem Function.Injective.right_inv_of_invOfMemRange

deleted def Mathlib.Meta.elabFinsetBuilderSetOf

deleted theorem Set.coe_toFinset

deleted def Set.decidableMemOfFintype

deleted theorem Set.disjoint_toFinset

deleted theorem Set.filter_mem_univ_eq_toFinset

deleted theorem Set.mem_toFinset

deleted theorem Set.ssubset_toFinset

deleted theorem Set.subset_toFinset

deleted def Set.toFinset

deleted theorem Set.toFinset_compl

deleted theorem Set.toFinset_congr

deleted theorem Set.toFinset_diff

deleted theorem Set.toFinset_empty

deleted theorem Set.toFinset_eq_empty

deleted theorem Set.toFinset_eq_univ

deleted theorem Set.toFinset_image

deleted theorem Set.toFinset_inj

deleted theorem Set.toFinset_insert

deleted theorem Set.toFinset_inter

deleted theorem Set.toFinset_nonempty

deleted theorem Set.toFinset_nontrivial

deleted theorem Set.toFinset_ofFinset

deleted theorem Set.toFinset_range

deleted theorem Set.toFinset_setOf

deleted theorem Set.toFinset_singleton

deleted theorem Set.toFinset_ssubset

deleted theorem Set.toFinset_ssubset_toFinset

deleted theorem Set.toFinset_ssubset_univ

deleted theorem Set.toFinset_subset

deleted theorem Set.toFinset_subset_toFinset

deleted theorem Set.toFinset_symmDiff

deleted theorem Set.toFinset_union

deleted theorem Set.toFinset_univ

deleted theorem mem_image_univ_iff_mem_range

deleted def precheckFinsetStx

deleted def setFintype

Modified Mathlib/Data/Fintype/Card.lean

Created Mathlib/Data/Fintype/Defs.lean

added theorem Finset.coe_eq_univ

added theorem Finset.coe_univ

added theorem Finset.eq_univ_iff_forall

added theorem Finset.eq_univ_of_forall

added theorem Finset.mem_univ

added theorem Finset.mem_univ_val

added theorem Finset.subset_univ

added def Finset.univ

added def Fintype.ofFinset

added def Mathlib.Meta.elabFinsetBuilderSetOf

Created Mathlib/Data/Fintype/Inv.lean

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.leftInverse_bijInv

added theorem Fintype.rightInverse_bijInv

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

Modified Mathlib/Data/Fintype/List.lean

Created Mathlib/Data/Fintype/OfMap.lean

added def Fintype.ofBijective

added def Fintype.ofEquiv

added def Fintype.ofIsEmpty

added def Fintype.ofList

added def Fintype.ofMultiset

added def Fintype.ofSubsingleton

added def Fintype.ofSurjective

added theorem Fintype.univ_ofIsEmpty

added theorem Fintype.univ_ofSubsingleton

Modified Mathlib/Data/Fintype/Quotient.lean

Created Mathlib/Data/Fintype/Sets.lean

added theorem Finset.attach_eq_univ

added theorem Finset.toFinset_coe

added theorem Finset.univ_eq_attach

added theorem Fintype.coe_finsetEquivSet

added theorem Fintype.coe_finsetOrderIsoSet

added theorem Fintype.coe_finsetOrderIsoSet_symm

added theorem Fintype.coe_image_univ

added theorem Fintype.finsetEquivSet_apply

added theorem Fintype.finsetEquivSet_symm_apply

added theorem Fintype.univ_Prop

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_nontrivial

added theorem Set.toFinset_ofFinset

added theorem Set.toFinset_range

added theorem Set.toFinset_setOf

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 mem_image_univ_iff_mem_range

added def precheckFinsetStx

added def setFintype

Modified Mathlib/Data/Fintype/Sigma.lean

Modified Mathlib/Data/List/Cycle.lean

Modified Mathlib/GroupTheory/FreeGroup/Reduce.lean

Modified Mathlib/Logic/Equiv/Fintype.lean

Modified Mathlib/Logic/Godel/GodelBetaFunction.lean

Modified Mathlib/RingTheory/IntegralDomain.lean