refactor(data/set/disjointed): split into data.set.pairwise and `or…

…der.disjointed` (#8411)

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

@@ -4,8 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Floris van Doorn
 -/
 import data.real.basic
-import data.set.disjointed
 import data.set.intervals
+import data.set.pairwise
 import set_theory.cardinal
 /-!
 Proof that a cube (in dimension n ≥ 3) cannot be cubed:

src/algebra/big_operators/finprod.lean

@@ -3,11 +3,9 @@ Copyright (c) 2020 Kexing Ying and Kevin Buzzard. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Kexing Ying, Kevin Buzzard, Yury Kudryashov
 -/
-
-import data.set.finite
-import data.set.disjointed
-import algebra.big_operators
+import algebra.big_operators.order
 import algebra.indicator_function
+import data.set.pairwise
 
 /-!
 # Finite products and sums over types and sets

src/data/equiv/encodable/lattice.lean

@@ -5,7 +5,7 @@ Authors: Floris van Doorn
 -/
 import data.equiv.encodable.basic
 import data.finset.basic
-import data.set.disjointed
+import data.set.pairwise
 
 /-!
 # Lattice operations on encodable types

src/data/mv_polynomial/variables.lean

@@ -5,7 +5,7 @@ Authors: Johannes Hölzl, Johan Commelin, Mario Carneiro
 -/
 import algebra.big_operators.order
 import data.mv_polynomial.monad
-import data.set.disjointed
+import data.set.pairwise
 
 /-!
 # Degrees and variables of polynomials

src/data/set/pairwise.lean

@@ -0,0 +1,61 @@
+/-
+Copyright (c) 2017 Johannes Hölzl. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Johannes Hölzl
+-/
+import data.set.lattice
+import tactic.wlog
+
+/-!
+# Relations holding pairwise
+
+This file defines pairwise relations.
+
+## Main declarations
+
+* `pairwise p`: States that `p i j` for all `i ≠ j`.
+
+-/
+open set
+
+universes u v w x
+variables {α : Type u} {β : Type v} {γ : Type w} {ι : Sort x}
+  {s t u : set α}
+
+/-- A relation `p` holds pairwise if `p i j` for all `i ≠ j`. -/
+def pairwise {α : Type*} (p : α → α → Prop) := ∀ i j, i ≠ j → p i j
+
+theorem set.pairwise_on_univ {r : α → α → Prop} :
+  (univ : set α).pairwise_on r ↔ pairwise r :=
+by simp only [pairwise_on, pairwise, mem_univ, forall_const]
+
+theorem set.pairwise_on.on_injective {s : set α} {r : α → α → Prop} (hs : pairwise_on s r)
+  {f : β → α} (hf : function.injective f) (hfs : ∀ x, f x ∈ s) :
+  pairwise (r on f) :=
+λ i j hij, hs _ (hfs i) _ (hfs j) (hf.ne hij)
+
+theorem pairwise.mono {p q : α → α → Prop} (h : ∀ ⦃i j⦄, p i j → q i j) (hp : pairwise p) :
+  pairwise q :=
+λ i j hij, h (hp i j hij)
+
+theorem pairwise_on_bool {r} (hr : symmetric r) {a b : α} :
+  pairwise (r on (λ c, cond c a b)) ↔ r a b :=
+by simpa [pairwise, function.on_fun] using @hr a b
+
+theorem pairwise_disjoint_on_bool [semilattice_inf_bot α] {a b : α} :
+  pairwise (disjoint on (λ c, cond c a b)) ↔ disjoint a b :=
+pairwise_on_bool disjoint.symm
+
+theorem pairwise_on_nat {r} (hr : symmetric r) (f : ℕ → α) :
+  pairwise (r on f) ↔ ∀ (m n) (h : m < n), r (f m) (f n) :=
+⟨λ p m n w, p m n w.ne, λ p m n w, by { wlog w' : m ≤ n, exact p m n ((ne.le_iff_lt w).mp w'), }⟩
+
+theorem pairwise_disjoint_on_nat [semilattice_inf_bot α] (f : ℕ → α) :
+  pairwise (disjoint on f) ↔ ∀ (m n) (h : m < n), disjoint (f m) (f n) :=
+pairwise_on_nat disjoint.symm f
+
+theorem pairwise.pairwise_on {p : α → α → Prop} (h : pairwise p) (s : set α) : s.pairwise_on p :=
+λ x hx y hy, h x y
+
+theorem pairwise_disjoint_fiber (f : α → β) : pairwise (disjoint on (λ y : β, f ⁻¹' {y})) :=
+set.pairwise_on_univ.1 $ pairwise_on_disjoint_fiber f univ

src/measure_theory/measurable_space.lean

@@ -6,6 +6,7 @@ Authors: Johannes Hölzl, Mario Carneiro
 
 import measure_theory.measurable_space_def
 import measure_theory.tactic
+import data.tprod
 
 
 /-!

src/measure_theory/measurable_space_def.lean

@@ -3,12 +3,11 @@ Copyright (c) 2017 Johannes Hölzl. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johannes Hölzl, Mario Carneiro
 -/
-import data.set.disjointed
-import data.set.countable
 import algebra.indicator_function
 import data.equiv.encodable.lattice
-import data.tprod
-import order.filter.lift
+import data.set.countable
+import order.disjointed
+import order.filter.basic
 import order.symm_diff
 
 /-!

src/data/set/disjointed.lean → src/order/disjointed.lean

@@ -1,67 +1,22 @@
 /-
 Copyright (c) 2017 Johannes Hölzl. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Johannes Hölzl
+Authors: Johannes Hölzl, Yaël Dillies
 -/
-import data.set.lattice
-import tactic.wlog
+import order.partial_sups
 
 /-!
-# Relations holding pairwise and consecutive differences of sets
+# Consecutive differences of sets
 
-This file defines pairwise relations and a way to make a sequence of sets into a sequence of
-disjoint sets.
+This file defines a way to make a sequence of sets into a sequence of disjoint sets.
 
 ## Main declarations
 
-* `pairwise p`: States that `p i j` for all `i ≠ j`.
 * `disjointed f`: Yields the sequence of sets `f 0`, `f 1 \ f 0`, `f 2 \ (f 0 ∪ f 1)`, ... This
   sequence has the same union as `f 0`, `f 1`, `f 2` but with disjoint sets.
-
 -/
-open set
-
-universes u v w x
-variables {α : Type u} {β : Type v} {γ : Type w} {ι : Sort x}
-  {s t u : set α}
-
-/-- A relation `p` holds pairwise if `p i j` for all `i ≠ j`. -/
-def pairwise {α : Type*} (p : α → α → Prop) := ∀ i j, i ≠ j → p i j
-
-theorem set.pairwise_on_univ {r : α → α → Prop} :
-  (univ : set α).pairwise_on r ↔ pairwise r :=
-by simp only [pairwise_on, pairwise, mem_univ, forall_const]
-
-theorem set.pairwise_on.on_injective {s : set α} {r : α → α → Prop} (hs : pairwise_on s r)
-  {f : β → α} (hf : function.injective f) (hfs : ∀ x, f x ∈ s) :
-  pairwise (r on f) :=
-λ i j hij, hs _ (hfs i) _ (hfs j) (hf.ne hij)
-
-theorem pairwise.mono {p q : α → α → Prop} (h : ∀ ⦃i j⦄, p i j → q i j) (hp : pairwise p) :
-  pairwise q :=
-λ i j hij, h (hp i j hij)
-
-theorem pairwise_on_bool {r} (hr : symmetric r) {a b : α} :
-  pairwise (r on (λ c, cond c a b)) ↔ r a b :=
-by simpa [pairwise, function.on_fun] using @hr a b
-
-theorem pairwise_disjoint_on_bool [semilattice_inf_bot α] {a b : α} :
-  pairwise (disjoint on (λ c, cond c a b)) ↔ disjoint a b :=
-pairwise_on_bool disjoint.symm
-
-theorem pairwise_on_nat {r} (hr : symmetric r) (f : ℕ → α) :
-  pairwise (r on f) ↔ ∀ (m n) (h : m < n), r (f m) (f n) :=
-⟨λ p m n w, p m n w.ne, λ p m n w, by { wlog w' : m ≤ n, exact p m n ((ne.le_iff_lt w).mp w'), }⟩
-
-theorem pairwise_disjoint_on_nat [semilattice_inf_bot α] (f : ℕ → α) :
-  pairwise (disjoint on f) ↔ ∀ (m n) (h : m < n), disjoint (f m) (f n) :=
-pairwise_on_nat disjoint.symm f
-
-theorem pairwise.pairwise_on {p : α → α → Prop} (h : pairwise p) (s : set α) : s.pairwise_on p :=
-λ x hx y hy, h x y
 
-theorem pairwise_disjoint_fiber (f : α → β) : pairwise (disjoint on (λ y : β, f ⁻¹' {y})) :=
-set.pairwise_on_univ.1 $ pairwise_on_disjoint_fiber f univ
+variables {α β : Type*}
 
 namespace set
 

src/order/partial_sups.lean

@@ -3,9 +3,9 @@ Copyright (c) 2021 Scott Morrison. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Scott Morrison
 -/
-import order.preorder_hom
 import data.finset.lattice
-import data.set.disjointed
+import data.set.pairwise
+import order.preorder_hom
 
 /-!
 # The monotone sequence of partial supremums of a sequence.

src/ring_theory/coprime.lean

@@ -3,11 +3,11 @@ Copyright (c) 2020 Kenny Lau. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Kenny Lau, Ken Lee, Chris Hughes
 -/
-import tactic.ring
 import algebra.big_operators.basic
 import data.fintype.basic
 import data.int.gcd
-import data.set.disjointed
+import data.set.pairwise
+import tactic.ring
 
 /-!
 # Coprime elements of a ring

src/topology/algebra/ordered/basic.lean

@@ -3,11 +3,12 @@ Copyright (c) 2017 Johannes Hölzl. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johannes Hölzl, Mario Carneiro, Yury Kudryashov
 -/
-import tactic.tfae
 import algebra.group_with_zero.power
 import data.set.intervals.pi
-import topology.algebra.group
 import order.filter.interval
+import topology.algebra.group
+import tactic.linarith
+import tactic.tfae
 
 /-!
 # Theory of topology on ordered spaces