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

added theorem Finset.codisjoint_left
added theorem Finset.coe_compl
added theorem Finset.coe_filter_univ
added theorem Finset.compl_empty
added theorem Finset.compl_erase
added theorem Finset.compl_filter
added theorem Finset.compl_insert
added theorem Finset.compl_inter
added theorem Finset.compl_singleton
added theorem Finset.compl_union
added theorem Finset.compl_univ
added theorem Finset.filter_univ_mem
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.mem_compl
added theorem Finset.not_mem_compl
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_inter
added theorem Finset.univ_nonempty
added theorem Finset.univ_nontrivial
added theorem Finset.univ_subset_iff
added theorem Finset.univ_unique
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_erase
deleted theorem Finset.compl_filter
deleted theorem Finset.compl_insert
deleted theorem Finset.compl_inter
deleted theorem Finset.compl_singleton
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.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.mem_compl
deleted theorem Finset.mem_univ
deleted theorem Finset.mem_univ_val
deleted theorem Finset.not_mem_compl
deleted theorem Finset.singleton_eq_univ
deleted theorem Finset.ssubset_univ_iff
deleted theorem Finset.subset_compl_comm
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_inter
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_subset_iff
deleted theorem Finset.univ_unique
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_image_univ
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 theorem Fintype.univ_Prop
deleted theorem Fintype.univ_ofIsEmpty
deleted theorem Set.coe_toFinset
deleted theorem Set.disjoint_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_univ
deleted theorem Set.toFinset_subset
deleted theorem Set.toFinset_symmDiff
deleted theorem Set.toFinset_union
deleted theorem Set.toFinset_univ
deleted def precheckFinsetStx
deleted def setFintype
added theorem Finset.attach_eq_univ
added theorem Finset.toFinset_coe
added theorem Finset.univ_eq_attach
added theorem Fintype.coe_image_univ
added theorem Fintype.univ_Prop
added theorem Set.coe_toFinset
added theorem Set.disjoint_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_setOf
added theorem Set.toFinset_singleton
added theorem Set.toFinset_ssubset
added theorem Set.toFinset_subset
added theorem Set.toFinset_symmDiff
added theorem Set.toFinset_union
added theorem Set.toFinset_univ
added def setFintype