Commit 2024-03-22 14:25 b7f0470e

chore(Set/Finset): standardize names of distributivity laws (#11572) Standardizes the following names for distributivity laws across Finset and Set:

• inter_union_distrib_left
• inter_union_distrib_right
• union_inter_distrib_left
• union_inter_distrib_right Makes arguments explicit in:
• Set.union_inter_distrib_right
• Set.union_inter_distrib_left
• Set.inter_union_distrib_right Deprecates these theorem names:
• Finset.inter_distrib_left
• Finset.inter_distrib_right
• Finset.union_distrib_right
• Finset.union_distrib_left
• Set.inter_distrib_left
• Set.inter_distrib_right
• Set.union_distrib_right
• Set.union_distrib_left Fixes use of deprecated names and implicit arguments in these files:
• Topology/Basic
• Topology/Connected/Basic
• MeasureTheory/MeasurableSpace/Basic
• MeasureTheory/Covering/Differentiation
• MeasureTheory/Constructions/BorelSpace/Basic
• Data/Set/Image
• Data/Set/Basic
• Data/PFun
• Data/Matroid/Dual
• Data/Finset/Sups
• Data/Finset/Basic
• Combinatorics/SetFamily/FourFunctions
• Combinatorics/Additive/SalemSpencer
• Counterexamples/Phillips.lean
• Archive/Imo/Imo2021Q1.lean