Commit 2023-03-27 21:46 39576edb

View on Github →

chore: Split data.set.pairwise (#3117) Match https://github.com/leanprover-community/mathlib/pull/17880 The new import of Mathlib.Data.Set.Lattice in Mathlib.Data.Finset.Basic was implied transitively from tactic imports present in Lean 3.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/BigOperators/Basic.lean

Modified Mathlib/Data/Finset/Basic.lean

Modified Mathlib/Data/Finset/Option.lean

Modified Mathlib/Data/List/Nodup.lean

Modified Mathlib/Data/Multiset/FinsetOps.lean

Modified Mathlib/Data/Prod/TProd.lean

Modified Mathlib/Data/Set/Intervals/Group.lean

Renamed Mathlib/Data/Set/Pairwise.lean to Mathlib/Data/Set/Pairwise/Basic.lean

deleted theorem Pairwise.bunionᵢ_injective

deleted theorem Pairwise.subset_of_bunionᵢ_subset_bunionᵢ

deleted theorem Set.PairwiseDisjoint.bunionᵢ

deleted theorem Set.PairwiseDisjoint.subset_of_bunionᵢ_subset_bunionᵢ

deleted theorem Set.bunionᵢ_diff_bunionᵢ_eq

deleted theorem Set.pairwiseDisjoint_unionᵢ

deleted theorem Set.pairwiseDisjoint_unionₛ

deleted theorem Set.pairwise_unionᵢ

deleted theorem Set.pairwise_unionₛ

Created Mathlib/Data/Set/Pairwise/Lattice.lean

added theorem Pairwise.bunionᵢ_injective

added theorem Pairwise.subset_of_bunionᵢ_subset_bunionᵢ

added theorem Set.PairwiseDisjoint.bunionᵢ

added theorem Set.PairwiseDisjoint.subset_of_bunionᵢ_subset_bunionᵢ

added theorem Set.bunionᵢ_diff_bunionᵢ_eq

added theorem Set.pairwiseDisjoint_unionᵢ

added theorem Set.pairwiseDisjoint_unionₛ

added theorem Set.pairwise_unionᵢ

added theorem Set.pairwise_unionₛ

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

Modified Mathlib/Order/Antichain.lean

Modified Mathlib/Order/Chain.lean

Modified Mathlib/Order/SuccPred/IntervalSucc.lean