Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2023-03-26 13:57 c227d107

View on Github →

chore(data/set/pairwise): split (#17880) This PR will split most of the lemmas in data.set.pairwise which are independent of the data.set.lattice. It makes a lot of files no longer depend on data.set.lattice. Zulip mathlib4 PR: https://github.com/leanprover-community/mathlib4/pull/1184

Estimated changes

Modified src/algebra/big_operators/basic.lean

Modified src/data/finset/option.lean

Modified src/data/list/nodup.lean

Modified src/data/multiset/finset_ops.lean

Modified src/data/prod/tprod.lean

Modified src/data/set/intervals/group.lean

Renamed src/data/set/pairwise.lean to src/data/set/pairwise/basic.lean

deleted theorem pairwise.bUnion_injective

deleted theorem pairwise.subset_of_bUnion_subset_bUnion

deleted theorem set.bUnion_diff_bUnion_eq

deleted theorem set.pairwise_Union

deleted theorem set.pairwise_disjoint.bUnion

deleted theorem set.pairwise_disjoint.subset_of_bUnion_subset_bUnion

deleted theorem set.pairwise_disjoint_Union

deleted theorem set.pairwise_disjoint_sUnion

deleted theorem set.pairwise_sUnion

Created src/data/set/pairwise/lattice.lean

added theorem pairwise.bUnion_injective

added theorem pairwise.subset_of_bUnion_subset_bUnion

added theorem set.bUnion_diff_bUnion_eq

added theorem set.pairwise_Union

added theorem set.pairwise_disjoint.bUnion

added theorem set.pairwise_disjoint.subset_of_bUnion_subset_bUnion

added theorem set.pairwise_disjoint_Union

added theorem set.pairwise_disjoint_sUnion

added theorem set.pairwise_sUnion

Modified src/data/set/pointwise/smul.lean

Modified src/order/antichain.lean

Modified src/order/chain.lean

Modified src/order/succ_pred/interval_succ.lean