Commit 2024-03-29 15:59 335f65c7

View on Github →

chore(Data/Finset/Basic): Depend on less order theory (#11732) Move Finset.biUnion and Finset.disjiUnion to a new file so that Data.Finset.Basic doesn't depend on that much order theory.

Estimated changes

deleted theorem Finset.Nonempty.biUnion
deleted theorem Finset.biUnion_biUnion
deleted theorem Finset.biUnion_congr
deleted theorem Finset.biUnion_empty
deleted theorem Finset.biUnion_insert
deleted theorem Finset.biUnion_inter
deleted theorem Finset.biUnion_mono
deleted theorem Finset.biUnion_nonempty
deleted theorem Finset.biUnion_subset
deleted theorem Finset.biUnion_val
deleted theorem Finset.bind_toFinset
deleted theorem Finset.coe_biUnion
deleted theorem Finset.coe_disjiUnion
deleted def Finset.disjiUnion
deleted theorem Finset.disjiUnion_cons
deleted theorem Finset.disjiUnion_empty
deleted theorem Finset.disjiUnion_val
deleted theorem Finset.erase_biUnion
deleted theorem Finset.filter_biUnion
deleted theorem Finset.inter_biUnion
deleted theorem Finset.mem_biUnion
deleted theorem Finset.mem_disjiUnion
deleted def Finset.piecewise
deleted theorem Finset.piecewise_cases
deleted theorem Finset.piecewise_coe
deleted theorem Finset.piecewise_congr
deleted theorem Finset.piecewise_empty
deleted theorem Finset.piecewise_insert
deleted theorem Finset.piecewise_mem_Icc'
deleted theorem Finset.piecewise_mem_Icc
deleted theorem Finset.piecewise_same
deleted theorem Finset.singleton_biUnion
deleted theorem Finset.update_piecewise
deleted theorem List.toFinset_range
deleted theorem Multiset.toFinset_range
added def Finset.piecewise
added theorem Finset.piecewise_cases
added theorem Finset.piecewise_coe
added theorem Finset.piecewise_compl
added theorem Finset.piecewise_congr
added theorem Finset.piecewise_empty
added theorem Finset.piecewise_same
added theorem Finset.piecewise_univ
added theorem Finset.biUnion_biUnion
added theorem Finset.biUnion_congr
added theorem Finset.biUnion_empty
added theorem Finset.biUnion_insert
added theorem Finset.biUnion_inter
added theorem Finset.biUnion_mono
added theorem Finset.biUnion_subset
added theorem Finset.biUnion_val
added theorem Finset.bind_toFinset
added theorem Finset.coe_biUnion
added theorem Finset.coe_disjiUnion
added theorem Finset.disjiUnion_cons
added theorem Finset.disjiUnion_val
added theorem Finset.erase_biUnion
added theorem Finset.filter_biUnion
added theorem Finset.inter_biUnion
added theorem Finset.mem_biUnion
added theorem Finset.mem_disjiUnion
deleted theorem Finset.piecewise_compl
deleted theorem Finset.piecewise_univ