Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-07-24 14:21 3d11f2da

View on Github →

refactor(data/set/disjointed): split into data.set.pairwise and order.disjointed (#8411)

Estimated changes

Modified archive/100-theorems-list/82_cubing_a_cube.lean

Modified src/algebra/big_operators/finprod.lean

Modified src/data/equiv/encodable/lattice.lean

Modified src/data/mv_polynomial/variables.lean

Created src/data/set/pairwise.lean

added theorem pairwise.mono

added theorem pairwise.pairwise_on

added def pairwise

added theorem pairwise_disjoint_fiber

added theorem pairwise_disjoint_on_bool

added theorem pairwise_disjoint_on_nat

added theorem pairwise_on_bool

added theorem pairwise_on_nat

added theorem set.pairwise_on.on_injective

added theorem set.pairwise_on_univ

Modified src/measure_theory/measurable_space.lean

Modified src/measure_theory/measurable_space_def.lean

Renamed src/data/set/disjointed.lean to src/order/disjointed.lean

deleted theorem pairwise.mono

deleted theorem pairwise.pairwise_on

deleted def pairwise

deleted theorem pairwise_disjoint_fiber

deleted theorem pairwise_disjoint_on_bool

deleted theorem pairwise_disjoint_on_nat

deleted theorem pairwise_on_bool

deleted theorem pairwise_on_nat

deleted theorem set.pairwise_on.on_injective

deleted theorem set.pairwise_on_univ

Modified src/order/partial_sups.lean

Modified src/ring_theory/coprime.lean

Modified src/topology/algebra/ordered/basic.lean