Commit 2023-10-06 15:59 c151d070

View on Github →

chore: clean up names with iUnion instead of Union (#7550)

Estimated changes

Modified Mathlib/Analysis/BoxIntegral/Box/SubboxInduction.lean

Modified Mathlib/Analysis/LocallyConvex/Basic.lean

Modified Mathlib/Data/Set/Pointwise/SMul.lean

deleted theorem Set.smul_set_Union

added theorem Set.smul_set_iUnion

Modified Mathlib/GroupTheory/Perm/Cycle/Basic.lean

deleted theorem Finset.product_self_eq_disjUnion_perm

deleted theorem Finset.product_self_eq_disj_Union_perm_aux

added theorem Finset.product_self_eq_disjiUnion_perm

added theorem Finset.product_self_eq_disjiUnion_perm_aux

Modified Mathlib/MeasureTheory/Group/FundamentalDomain.lean

Modified Mathlib/Order/Concept.lean

deleted theorem extentClosure_Union₂

added theorem extentClosure_iUnion₂

Modified Mathlib/Order/ConditionallyCompleteLattice/Basic.lean

deleted theorem Monotone.ciSup_mem_Inter_Icc_of_antitone

added theorem Monotone.ciSup_mem_iInter_Icc_of_antitone

deleted theorem ciSup_mem_Inter_Icc_of_antitone_Icc

added theorem ciSup_mem_iInter_Icc_of_antitone_Icc

Modified Mathlib/Order/Filter/CountableInter.lean

Modified Mathlib/Probability/Kernel/CondCdf.lean

Modified Mathlib/Topology/Basic.lean

deleted theorem closure_Union_of_finite

added theorem closure_iUnion_of_finite

deleted theorem interior_Inter₂_subset

added theorem interior_iInter₂_subset

Modified Mathlib/Topology/Separation.lean