chore(data/set/pairwise): rename set.pairwise_on to set.pairwise to match list.pairwise and multiset.pairwise (#10035)

Author: eric-wieser

src/algebra/big_operators/finprod.lean

@@ -699,7 +699,7 @@ sets `t i`, `i ∈ I`, are finite, if all `t i`, `i ∈ I`, are pairwise disjoin
 the product of `f a` over `a ∈ ⋃ i ∈ I, t i` is equal to the product over `i ∈ I`
 of the products of `f a` over `a ∈ t i`. -/
 @[to_additive] lemma finprod_mem_bUnion {I : set ι} {t : ι → set α}
-  (h : pairwise_on I (disjoint on t)) (hI : I.finite) (ht : ∀ i ∈ I, (t i).finite) :
+  (h : I.pairwise (disjoint on t)) (hI : I.finite) (ht : ∀ i ∈ I, (t i).finite) :
   ∏ᶠ a ∈ ⋃ x ∈ I, t x, f a = ∏ᶠ i ∈ I, ∏ᶠ j ∈ t i, f j :=
 begin
   haveI := hI.fintype,
@@ -709,7 +709,7 @@ end
 
 /-- If `t` is a finite set of pairwise disjoint finite sets, then the product of `f a`
 over `a ∈ ⋃₀ t` is the product over `s ∈ t` of the products of `f a` over `a ∈ s`. -/
-@[to_additive] lemma finprod_mem_sUnion {t : set (set α)} (h : pairwise_on t disjoint)
+@[to_additive] lemma finprod_mem_sUnion {t : set (set α)} (h : t.pairwise disjoint)
   (ht₀ : t.finite) (ht₁ : ∀ x ∈ t, set.finite x):
   ∏ᶠ a ∈ ⋃₀ t, f a = ∏ᶠ s ∈ t, ∏ᶠ a ∈ s, f a :=
 by rw [set.sUnion_eq_bUnion, finprod_mem_bUnion h ht₀ ht₁]

src/analysis/box_integral/partition/basic.lean

@@ -47,7 +47,7 @@ variables {ι : Type*}
 structure prepartition (I : box ι) :=
 (boxes : finset (box ι))
 (le_of_mem' : ∀ J ∈ boxes, J ≤ I)
-(pairwise_disjoint : pairwise_on ↑boxes (disjoint on (coe : box ι → set (ι → ℝ))))
+(pairwise_disjoint : set.pairwise ↑boxes (disjoint on (coe : box ι → set (ι → ℝ))))
 
 namespace prepartition
 
@@ -224,7 +224,7 @@ function. -/
     end,
   pairwise_disjoint :=
     begin
-      simp only [pairwise_on, finset.mem_coe, finset.mem_bUnion],
+      simp only [set.pairwise, finset.mem_coe, finset.mem_bUnion],
       rintro J₁' ⟨J₁, hJ₁, hJ₁'⟩ J₂' ⟨J₂, hJ₂, hJ₂'⟩ Hne x ⟨hx₁, hx₂⟩, apply Hne,
       obtain rfl : J₁ = J₂,
         from π.eq_of_mem_of_mem hJ₁ hJ₂ ((πi J₁).le_of_mem hJ₁' hx₁)
@@ -308,7 +308,7 @@ end
 the empty one if it exists. -/
 def of_with_bot (boxes : finset (with_bot (box ι)))
   (le_of_mem : ∀ J ∈ boxes, (J : with_bot (box ι)) ≤ I)
-  (pairwise_disjoint : pairwise_on (boxes : set (with_bot (box ι))) disjoint) :
+  (pairwise_disjoint : set.pairwise (boxes : set (with_bot (box ι))) disjoint) :
   prepartition I :=
 { boxes := boxes.erase_none,
   le_of_mem' := λ J hJ,
@@ -328,7 +328,7 @@ mem_erase_none
 
 @[simp] lemma Union_of_with_bot (boxes : finset (with_bot (box ι)))
   (le_of_mem : ∀ J ∈ boxes, (J : with_bot (box ι)) ≤ I)
-  (pairwise_disjoint : pairwise_on (boxes : set (with_bot (box ι))) disjoint) :
+  (pairwise_disjoint : set.pairwise (boxes : set (with_bot (box ι))) disjoint) :
   (of_with_bot boxes le_of_mem pairwise_disjoint).Union = ⋃ J ∈ boxes, ↑J :=
 begin
   suffices : (⋃ (J : box ι) (hJ : ↑J ∈ boxes), ↑J) = ⋃ J ∈ boxes, ↑J,
@@ -339,7 +339,7 @@ end
 
 lemma of_with_bot_le {boxes : finset (with_bot (box ι))}
   {le_of_mem : ∀ J ∈ boxes, (J : with_bot (box ι)) ≤ I}
-  {pairwise_disjoint : pairwise_on (boxes : set (with_bot (box ι))) disjoint}
+  {pairwise_disjoint : set.pairwise (boxes : set (with_bot (box ι))) disjoint}
   (H : ∀ J ∈ boxes, J ≠ ⊥ → ∃ J' ∈ π, J ≤ ↑J') :
   of_with_bot boxes le_of_mem pairwise_disjoint ≤ π :=
 have ∀ (J : box ι), ↑J ∈ boxes → ∃ J' ∈ π, J ≤ J',
@@ -348,7 +348,7 @@ by simpa [of_with_bot, le_def]
 
 lemma le_of_with_bot {boxes : finset (with_bot (box ι))}
   {le_of_mem : ∀ J ∈ boxes, (J : with_bot (box ι)) ≤ I}
-  {pairwise_disjoint : pairwise_on (boxes : set (with_bot (box ι))) disjoint}
+  {pairwise_disjoint : set.pairwise (boxes : set (with_bot (box ι))) disjoint}
   (H : ∀ J ∈ π, ∃ J' ∈ boxes, ↑J ≤ J') :
   π ≤ of_with_bot boxes le_of_mem pairwise_disjoint :=
 begin
@@ -360,10 +360,10 @@ end
 
 lemma of_with_bot_mono {boxes₁ : finset (with_bot (box ι))}
   {le_of_mem₁ : ∀ J ∈ boxes₁, (J : with_bot (box ι)) ≤ I}
-  {pairwise_disjoint₁ : pairwise_on (boxes₁ : set (with_bot (box ι))) disjoint}
+  {pairwise_disjoint₁ : set.pairwise (boxes₁ : set (with_bot (box ι))) disjoint}
   {boxes₂ : finset (with_bot (box ι))}
   {le_of_mem₂ : ∀ J ∈ boxes₂, (J : with_bot (box ι)) ≤ I}
-  {pairwise_disjoint₂ : pairwise_on (boxes₂ : set (with_bot (box ι))) disjoint}
+  {pairwise_disjoint₂ : set.pairwise (boxes₂ : set (with_bot (box ι))) disjoint}
   (H : ∀ J ∈ boxes₁, J ≠ ⊥ → ∃ J' ∈ boxes₂, J ≤ J') :
   of_with_bot boxes₁ le_of_mem₁ pairwise_disjoint₁ ≤
     of_with_bot boxes₂ le_of_mem₂ pairwise_disjoint₂ :=
@@ -372,7 +372,7 @@ le_of_with_bot _ $ λ J hJ, H J (mem_of_with_bot.1 hJ) (with_bot.coe_ne_bot _)
 lemma sum_of_with_bot {M : Type*} [add_comm_monoid M]
   (boxes : finset (with_bot (box ι)))
   (le_of_mem : ∀ J ∈ boxes, (J : with_bot (box ι)) ≤ I)
-  (pairwise_disjoint : pairwise_on (boxes : set (with_bot (box ι))) disjoint)
+  (pairwise_disjoint : set.pairwise (boxes : set (with_bot (box ι))) disjoint)
   (f : box ι → M) :
   ∑ J in (of_with_bot boxes le_of_mem pairwise_disjoint).boxes, f J =
     ∑ J in boxes, option.elim J 0 f :=
@@ -384,7 +384,7 @@ def restrict (π : prepartition I) (J : box ι) :
 of_with_bot (π.boxes.image (λ J', J ⊓ J'))
   (λ J' hJ', by { rcases finset.mem_image.1 hJ' with ⟨J', -, rfl⟩, exact inf_le_left })
   begin
-    simp only [pairwise_on, on_fun, finset.mem_coe, finset.mem_image],
+    simp only [set.pairwise, on_fun, finset.mem_coe, finset.mem_image],
     rintro _ ⟨J₁, h₁, rfl⟩ _ ⟨J₂, h₂, rfl⟩ Hne,
     have : J₁ ≠ J₂, by { rintro rfl, exact Hne rfl },
     exact ((box.disjoint_coe.2 $ π.disjoint_coe_of_mem h₁ h₂ this).inf_left' _).inf_right' _
@@ -523,7 +523,7 @@ by convert sum_fiberwise_of_maps_to (λ _, finset.mem_image_of_mem f) g
   le_of_mem' := λ J hJ, (finset.mem_union.1 hJ).elim π₁.le_of_mem π₂.le_of_mem,
   pairwise_disjoint :=
     suffices ∀ (J₁ ∈ π₁) (J₂ ∈ π₂), J₁ ≠ J₂ → disjoint (J₁ : set (ι → ℝ)) J₂,
-      by simpa [pairwise_on_union_of_symmetric (symmetric_disjoint.comap _), pairwise_disjoint],
+      by simpa [pairwise_union_of_symmetric (symmetric_disjoint.comap _), pairwise_disjoint],
     λ J₁ h₁ J₂ h₂ _, h.mono (π₁.subset_Union h₁) (π₂.subset_Union h₂) }
 
 @[simp] lemma mem_disj_union (H : disjoint π₁.Union π₂.Union) :

src/analysis/box_integral/partition/split.lean

@@ -147,7 +147,7 @@ of_with_bot {I.split_lower i x, I.split_upper i x}
   end
   begin
     simp only [finset.coe_insert, finset.coe_singleton, true_and, set.mem_singleton_iff,
-     pairwise_on_insert_of_symmetric symmetric_disjoint, pairwise_on_singleton],
+      pairwise_insert_of_symmetric symmetric_disjoint, pairwise_singleton],
     rintro J rfl -,
     exact I.disjoint_split_lower_split_upper i x
   end

src/analysis/convex/basic.lean

@@ -529,8 +529,8 @@ begin
   exact h hx hy ha hb hab
 end
 
-lemma convex_iff_pairwise_on_pos :
-  convex 𝕜 s ↔ s.pairwise_on (λ x y, ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → a + b = 1 → a • x + b • y ∈ s) :=
+lemma convex_iff_pairwise_pos :
+  convex 𝕜 s ↔ s.pairwise (λ x y, ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → a + b = 1 → a • x + b • y ∈ s) :=
 begin
   refine ⟨λ h x hx y hy _ a b ha hb hab, h hx hy ha.le hb.le hab, _⟩,
   intros h x y hx hy a b ha hb hab,

src/analysis/convex/function.lean

@@ -229,9 +229,9 @@ lemma concave_on_iff_forall_pos {s : set E} {f : E → β} :
     → a • f x + b • f y ≤ f (a • x + b • y) :=
 @convex_on_iff_forall_pos 𝕜 E (order_dual β) _ _ _ _ _ _ _
 
-lemma convex_on_iff_pairwise_on_pos {s : set E} {f : E → β} :
+lemma convex_on_iff_pairwise_pos {s : set E} {f : E → β} :
   convex_on 𝕜 s f ↔ convex 𝕜 s ∧
-    s.pairwise_on (λ x y, ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → a + b = 1
+    s.pairwise (λ x y, ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → a + b = 1
     → f (a • x + b • y) ≤ a • f x + b • f y) :=
 begin
   rw convex_on_iff_forall_pos,
@@ -242,11 +242,11 @@ begin
   exact h x hx y hy hxy ha hb hab,
 end
 
-lemma concave_on_iff_pairwise_on_pos {s : set E} {f : E → β} :
+lemma concave_on_iff_pairwise_pos {s : set E} {f : E → β} :
   concave_on 𝕜 s f ↔ convex 𝕜 s ∧
-   s.pairwise_on (λ x y, ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → a + b = 1
+   s.pairwise (λ x y, ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → a + b = 1
     → a • f x + b • f y ≤ f (a • x + b • y)) :=
-@convex_on_iff_pairwise_on_pos 𝕜 E (order_dual β) _ _ _ _ _ _ _
+@convex_on_iff_pairwise_pos 𝕜 E (order_dual β) _ _ _ _ _ _ _
 
 /-- A linear map is convex. -/
 lemma linear_map.convex_on (f : E →ₗ[𝕜] β) {s : set E} (hs : convex 𝕜 s) : convex_on 𝕜 s f :=
@@ -279,7 +279,7 @@ variables [ordered_smul 𝕜 β] {s : set E} {f : E → β}
 
 lemma strict_convex_on.convex_lt (hf : strict_convex_on 𝕜 s f) (r : β) :
   convex 𝕜 {x ∈ s | f x < r} :=
-convex_iff_pairwise_on_pos.2 $ λ x hx y hy hxy a b ha hb hab, ⟨hf.1 hx.1 hy.1 ha.le hb.le hab,
+convex_iff_pairwise_pos.2 $ λ x hx y hy hxy a b ha hb hab, ⟨hf.1 hx.1 hy.1 ha.le hb.le hab,
   calc
     f (a • x + b • y) < a • f x + b • f y : hf.2 hx.1 hy.1 hxy ha hb hab
                   ... ≤ a • r + b • r     : add_le_add (smul_lt_smul_of_pos hx.2 ha).le
@@ -304,7 +304,7 @@ lemma linear_order.convex_on_of_lt (hs : convex 𝕜 s)
   (hf : ∀ ⦃x y : E⦄, x ∈ s → y ∈ s → x < y → ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → a + b = 1 →
     f (a • x + b • y) ≤ a • f x + b • f y) : convex_on 𝕜 s f :=
 begin
-  refine convex_on_iff_pairwise_on_pos.2 ⟨hs, λ x hx y hy hxy a b ha hb hab, _⟩,
+  refine convex_on_iff_pairwise_pos.2 ⟨hs, λ x hx y hy hxy a b ha hb hab, _⟩,
   wlog h : x ≤ y using [x y a b, y x b a],
   { exact le_total _ _ },
   exact hf hx hy (h.lt_of_ne hxy) ha hb hab,

src/data/list/nodup.lean

@@ -338,8 +338,8 @@ begin
   exact absurd (hl x) hx.not_le
 end
 
-lemma nodup.pairwise_of_set_pairwise_on {l : list α} {r : α → α → Prop}
-  (hl : l.nodup) (h : {x | x ∈ l}.pairwise_on r) : l.pairwise r :=
+lemma nodup.pairwise_of_set_pairwise {l : list α} {r : α → α → Prop}
+  (hl : l.nodup) (h : {x | x ∈ l}.pairwise r) : l.pairwise r :=
 hl.pairwise_of_forall_ne h
 
 end list

src/data/list/pairwise.lean

@@ -246,8 +246,8 @@ from λ R l, ⟨λ p, reverse_reverse l ▸ this p, this⟩,
     pairwise_cons, forall_prop_of_false (not_mem_nil _), forall_true_iff,
     pairwise.nil, mem_reverse, mem_singleton, forall_eq, true_and] using h]
 
-lemma pairwise.set_pairwise_on {l : list α} (h : pairwise R l) (hr : symmetric R) :
-  set.pairwise_on {x | x ∈ l} R :=
+lemma pairwise.set_pairwise {l : list α} (h : pairwise R l) (hr : symmetric R) :
+  set.pairwise {x | x ∈ l} R :=
 begin
   induction h with hd tl imp h IH,
   { simp },

src/data/polynomial/field_division.lean

@@ -408,7 +408,7 @@ begin
     pairwise_coprime_X_sub function.injective_id,
   have H : pairwise (is_coprime on λ (a : R), (polynomial.X - C (id a)) ^ (root_multiplicity a p)),
   { intros a b hdiff, exact (hcoprime a b hdiff).pow },
-  apply finset.prod_dvd_of_coprime (pairwise.pairwise_on H (↑(multiset.to_finset p.roots) : set R)),
+  apply finset.prod_dvd_of_coprime (H.set_pairwise (↑(multiset.to_finset p.roots) : set R)),
   intros a h,
   rw multiset.mem_to_finset at h,
   exact pow_root_multiplicity_dvd p a