chore(order/*): rename strict_mono_{incr,decr}_on to `strict_{mono,…

…anti}_on` (#9401)

This was done as a direct find and replace

archive/100-theorems-list/73_ascending_descending_sequences.lean

@@ -39,20 +39,20 @@ We then show the pair of labels must be unique. Now if there is no increasing se
 which is a contradiction if there are more than `r * s` elements.
 -/
 theorem erdos_szekeres {r s n : ℕ} {f : fin n → α} (hn : r * s < n) (hf : injective f) :
-  (∃ (t : finset (fin n)), r < t.card ∧ strict_mono_incr_on f ↑t) ∨
-  (∃ (t : finset (fin n)), s < t.card ∧ strict_mono_decr_on f ↑t) :=
+  (∃ (t : finset (fin n)), r < t.card ∧ strict_mono_on f ↑t) ∨
+  (∃ (t : finset (fin n)), s < t.card ∧ strict_anti_on f ↑t) :=
 begin
   -- Given an index `i`, produce the set of increasing (resp., decreasing) subsequences which ends
   -- at `i`.
   let inc_sequences_ending_in : fin n → finset (finset (fin n)) :=
-    λ i, univ.powerset.filter (λ t, finset.max t = some i ∧ strict_mono_incr_on f ↑t),
+    λ i, univ.powerset.filter (λ t, finset.max t = some i ∧ strict_mono_on f ↑t),
   let dec_sequences_ending_in : fin n → finset (finset (fin n)) :=
-    λ i, univ.powerset.filter (λ t, finset.max t = some i ∧ strict_mono_decr_on f ↑t),
+    λ i, univ.powerset.filter (λ t, finset.max t = some i ∧ strict_anti_on f ↑t),
   -- The singleton sequence is in both of the above collections.
   -- (This is useful to show that the maximum length subsequence is at least 1, and that the set
   -- of subsequences is nonempty.)
-  have inc_i : ∀ i, {i} ∈ inc_sequences_ending_in i := λ i, by simp [strict_mono_incr_on],
-  have dec_i : ∀ i, {i} ∈ dec_sequences_ending_in i := λ i, by simp [strict_mono_decr_on],
+  have inc_i : ∀ i, {i} ∈ inc_sequences_ending_in i := λ i, by simp [strict_mono_on],
+  have dec_i : ∀ i, {i} ∈ dec_sequences_ending_in i := λ i, by simp [strict_anti_on],
   -- Define the pair of labels: at index `i`, the pair is the maximum length of an increasing
   -- subsequence ending at `i`, paired with the maximum length of a decreasing subsequence ending
   -- at `i`.
@@ -110,7 +110,7 @@ begin
           apply le_of_lt ‹i < j› },
         -- To show it's increasing (i.e., `f` is monotone increasing on `t.insert j`), we do cases
         -- on what the possibilities could be - either in `t` or equals `j`.
-        simp only [strict_mono_incr_on, strict_mono_decr_on, coe_insert, set.mem_insert_iff,
+        simp only [strict_mono_on, strict_anti_on, coe_insert, set.mem_insert_iff,
           mem_coe],
         -- Most of the cases are just bashes.
         rintros x ⟨rfl | _⟩ y ⟨rfl | _⟩ _,

src/algebra/group_power/order.lean

@@ -161,8 +161,8 @@ begin
   { rw [←h, zero_pow Hnpos], apply pow_pos (by rwa ←h at Hxy : 0 < y),}
 end
 
-theorem strict_mono_incr_on_pow {n : ℕ} (hn : 0 < n) :
-  strict_mono_incr_on (λ x : R, x ^ n) (set.Ici 0) :=
+theorem strict_mono_on_pow {n : ℕ} (hn : 0 < n) :
+  strict_mono_on (λ x : R, x ^ n) (set.Ici 0) :=
 λ x hx y hy h, pow_lt_pow_of_lt_left h hx hn
 
 theorem one_le_pow_of_one_le {a : R} (H : 1 ≤ a) : ∀ (n : ℕ), 1 ≤ a ^ n
@@ -200,7 +200,7 @@ variable [linear_ordered_semiring R]
 
 @[simp] theorem pow_left_inj {x y : R} {n : ℕ} (Hxpos : 0 ≤ x) (Hypos : 0 ≤ y) (Hnpos : 0 < n) :
   x ^ n = y ^ n ↔ x = y :=
-(@strict_mono_incr_on_pow R _ _ Hnpos).inj_on.eq_iff Hxpos Hypos
+(@strict_mono_on_pow R _ _ Hnpos).inj_on.eq_iff Hxpos Hypos
 
 lemma lt_of_pow_lt_pow {a b : R} (n : ℕ) (hb : 0 ≤ b) (h : a ^ n < b ^ n) : a < b :=
 lt_of_not_ge $ λ hn, not_lt_of_ge (pow_le_pow_of_le_left hb hn _) h

src/algebra/order/field.lean

@@ -695,7 +695,7 @@ lemma abs_inv (a : α) : abs a⁻¹ = (abs a)⁻¹ :=
 (abs_hom : monoid_with_zero_hom α α).map_inv' a
 
 -- TODO: add lemmas with `a⁻¹`.
-lemma one_div_strict_mono_decr_on : strict_mono_decr_on (λ x : α, 1 / x) (set.Ioi 0) :=
+lemma one_div_strict_anti_on : strict_anti_on (λ x : α, 1 / x) (set.Ioi 0) :=
 λ x x1 y y1 xy, (one_div_lt_one_div (set.mem_Ioi.mp y1) (set.mem_Ioi.mp x1)).mpr xy
 
 lemma one_div_pow_le_one_div_pow_of_le (a1 : 1 ≤ a) {m n : ℕ} (mn : m ≤ n) :

src/algebra/order/ring.lean

@@ -259,11 +259,11 @@ lemma mul_self_lt_mul_self (h1 : 0 ≤ a) (h2 : a < b) : a * a < b * b :=
 mul_lt_mul' h2.le h2 h1 $ h1.trans_lt h2
 
 -- See Note [decidable namespace]
-protected lemma decidable.strict_mono_incr_on_mul_self [@decidable_rel α (≤)] :
-  strict_mono_incr_on (λ x : α, x * x) (set.Ici 0) :=
+protected lemma decidable.strict_mono_on_mul_self [@decidable_rel α (≤)] :
+  strict_mono_on (λ x : α, x * x) (set.Ici 0) :=
 λ x hx y hy hxy, decidable.mul_self_lt_mul_self hx hxy
 
-lemma strict_mono_incr_on_mul_self : strict_mono_incr_on (λ x : α, x * x) (set.Ici 0) :=
+lemma strict_mono_on_mul_self : strict_mono_on (λ x : α, x * x) (set.Ici 0) :=
 λ x hx y hy hxy, mul_self_lt_mul_self hx hxy
 
 -- See Note [decidable namespace]
@@ -1122,11 +1122,11 @@ by haveI := @linear_order.decidable_le α _; exact
 
 lemma mul_self_lt_mul_self_iff {a b : α} (h1 : 0 ≤ a) (h2 : 0 ≤ b) : a < b ↔ a * a < b * b :=
 by haveI := @linear_order.decidable_le α _; exact
-((@decidable.strict_mono_incr_on_mul_self α _ _).lt_iff_lt h1 h2).symm
+((@decidable.strict_mono_on_mul_self α _ _).lt_iff_lt h1 h2).symm
 
 lemma mul_self_inj {a b : α} (h1 : 0 ≤ a) (h2 : 0 ≤ b) : a * a = b * b ↔ a = b :=
 by haveI := @linear_order.decidable_le α _; exact
-(@decidable.strict_mono_incr_on_mul_self α _ _).inj_on.eq_iff h1 h2
+(@decidable.strict_mono_on_mul_self α _ _).inj_on.eq_iff h1 h2
 
 @[simp] lemma mul_le_mul_left_of_neg {a b c : α} (h : c < 0) : c * a ≤ c * b ↔ b ≤ a :=
 by haveI := @linear_order.decidable_le α _; exact

src/analysis/special_functions/exp_log.lean

@@ -462,10 +462,10 @@ end
 lemma log_nonpos (hx : 0 ≤ x) (h'x : x ≤ 1) : log x ≤ 0 :=
 (log_nonpos_iff' hx).2 h'x
 
-lemma strict_mono_incr_on_log : strict_mono_incr_on log (set.Ioi 0) :=
+lemma strict_mono_on_log : strict_mono_on log (set.Ioi 0) :=
 λ x hx y hy hxy, log_lt_log hx hxy
 
-lemma strict_mono_decr_on_log : strict_mono_decr_on log (set.Iio 0) :=
+lemma strict_anti_on_log : strict_anti_on log (set.Iio 0) :=
 begin
   rintros x (hx : x < 0) y (hy : y < 0) hxy,
   rw [← log_abs y, ← log_abs x],
@@ -474,7 +474,7 @@ begin
 end
 
 lemma log_inj_on_pos : set.inj_on log (set.Ioi 0) :=
-strict_mono_incr_on_log.inj_on
+strict_mono_on_log.inj_on
 
 lemma eq_one_of_pos_of_log_eq_zero {x : ℝ} (h₁ : 0 < x) (h₂ : log x = 0) : x = 1 :=
 log_inj_on_pos (set.mem_Ioi.2 h₁) (set.mem_Ioi.2 zero_lt_one) (h₂.trans real.log_one.symm)

src/analysis/special_functions/trigonometric/arctan.lean

@@ -120,7 +120,7 @@ univ_subset_iff.1 surj_on_tan
 
 /-- `real.tan` as an `order_iso` between `(-(π / 2), π / 2)` and `ℝ`. -/
 def tan_order_iso : Ioo (-(π / 2)) (π / 2) ≃o ℝ :=
-(strict_mono_incr_on_tan.order_iso _ _).trans $ (order_iso.set_congr _ _ image_tan_Ioo).trans
+(strict_mono_on_tan.order_iso _ _).trans $ (order_iso.set_congr _ _ image_tan_Ioo).trans
   order_iso.set.univ
 
 /-- Inverse of the `tan` function, returns values in the range `-π / 2 < arctan x` and

src/analysis/special_functions/trigonometric/basic.lean

@@ -1281,29 +1281,29 @@ match (le_total x (π / 2) : x ≤ π / 2 ∨ π / 2 ≤ x), le_total y (π / 2)
   apply cos_lt_cos_of_nonneg_of_le_pi_div_two; linarith)
 end
 
-lemma strict_mono_decr_on_cos : strict_mono_decr_on cos (Icc 0 π) :=
+lemma strict_anti_on_cos : strict_anti_on cos (Icc 0 π) :=
 λ x hx y hy hxy, cos_lt_cos_of_nonneg_of_le_pi hx.1 hy.2 hxy
 
 lemma cos_le_cos_of_nonneg_of_le_pi {x y : ℝ} (hx₁ : 0 ≤ x) (hy₂ : y ≤ π) (hxy : x ≤ y) :
   cos y ≤ cos x :=
-(strict_mono_decr_on_cos.le_iff_le ⟨hx₁.trans hxy, hy₂⟩ ⟨hx₁, hxy.trans hy₂⟩).2 hxy
+(strict_anti_on_cos.le_iff_le ⟨hx₁.trans hxy, hy₂⟩ ⟨hx₁, hxy.trans hy₂⟩).2 hxy
 
 lemma sin_lt_sin_of_lt_of_le_pi_div_two {x y : ℝ} (hx₁ : -(π / 2) ≤ x)
   (hy₂ : y ≤ π / 2) (hxy : x < y) : sin x < sin y :=
 by rw [← cos_sub_pi_div_two, ← cos_sub_pi_div_two, ← cos_neg (x - _), ← cos_neg (y - _)];
   apply cos_lt_cos_of_nonneg_of_le_pi; linarith
 
-lemma strict_mono_incr_on_sin : strict_mono_incr_on sin (Icc (-(π / 2)) (π / 2)) :=
+lemma strict_mono_on_sin : strict_mono_on sin (Icc (-(π / 2)) (π / 2)) :=
 λ x hx y hy hxy, sin_lt_sin_of_lt_of_le_pi_div_two hx.1 hy.2 hxy
 
 lemma sin_le_sin_of_le_of_le_pi_div_two {x y : ℝ} (hx₁ : -(π / 2) ≤ x)
   (hy₂ : y ≤ π / 2) (hxy : x ≤ y) : sin x ≤ sin y :=
-(strict_mono_incr_on_sin.le_iff_le ⟨hx₁, hxy.trans hy₂⟩ ⟨hx₁.trans hxy, hy₂⟩).2 hxy
+(strict_mono_on_sin.le_iff_le ⟨hx₁, hxy.trans hy₂⟩ ⟨hx₁.trans hxy, hy₂⟩).2 hxy
 
 lemma inj_on_sin : inj_on sin (Icc (-(π / 2)) (π / 2)) :=
-strict_mono_incr_on_sin.inj_on
+strict_mono_on_sin.inj_on
 
-lemma inj_on_cos : inj_on cos (Icc 0 π) := strict_mono_decr_on_cos.inj_on
+lemma inj_on_cos : inj_on cos (Icc 0 π) := strict_anti_on_cos.inj_on
 
 lemma surj_on_sin : surj_on sin (Icc (-(π / 2)) (π / 2)) (Icc (-1) 1) :=
 by simpa only [sin_neg, sin_pi_div_two]
@@ -1661,7 +1661,7 @@ end angle
 
 /-- `real.sin` as an `order_iso` between `[-(π / 2), π / 2]` and `[-1, 1]`. -/
 def sin_order_iso : Icc (-(π / 2)) (π / 2) ≃o Icc (-1:ℝ) 1 :=
-(strict_mono_incr_on_sin.order_iso _ _).trans $ order_iso.set_congr _ _ bij_on_sin.image_eq
+(strict_mono_on_sin.order_iso _ _).trans $ order_iso.set_congr _ _ bij_on_sin.image_eq
 
 @[simp] lemma coe_sin_order_iso_apply (x : Icc (-(π / 2)) (π / 2)) :
   (sin_order_iso x : ℝ) = sin x := rfl
@@ -1723,11 +1723,11 @@ match le_total x 0, le_total y 0 with
 | or.inr hx0, or.inr hy0 := tan_lt_tan_of_nonneg_of_lt_pi_div_two hx0 hy₂ hxy
 end
 
-lemma strict_mono_incr_on_tan : strict_mono_incr_on tan (Ioo (-(π / 2)) (π / 2)) :=
+lemma strict_mono_on_tan : strict_mono_on tan (Ioo (-(π / 2)) (π / 2)) :=
 λ x hx y hy, tan_lt_tan_of_lt_of_lt_pi_div_two hx.1 hy.2
 
 lemma inj_on_tan : inj_on tan (Ioo (-(π / 2)) (π / 2)) :=
-strict_mono_incr_on_tan.inj_on
+strict_mono_on_tan.inj_on
 
 lemma tan_inj_of_lt_of_lt_pi_div_two {x y : ℝ} (hx₁ : -(π / 2) < x) (hx₂ : x < π / 2)
   (hy₁ : -(π / 2) < y) (hy₂ : y < π / 2) (hxy : tan x = tan y) : x = y :=

src/analysis/special_functions/trigonometric/inverse.lean

@@ -53,14 +53,14 @@ inj_on_sin (arcsin_mem_Icc _) hx $ by rw [sin_arcsin (neg_one_le_sin _) (sin_le_
 lemma arcsin_sin {x : ℝ} (hx₁ : -(π / 2) ≤ x) (hx₂ : x ≤ π / 2) : arcsin (sin x) = x :=
 arcsin_sin' ⟨hx₁, hx₂⟩
 
-lemma strict_mono_incr_on_arcsin : strict_mono_incr_on arcsin (Icc (-1) 1) :=
-(subtype.strict_mono_coe _).comp_strict_mono_incr_on $
-  sin_order_iso.symm.strict_mono.strict_mono_incr_on_Icc_extend _
+lemma strict_mono_on_arcsin : strict_mono_on arcsin (Icc (-1) 1) :=
+(subtype.strict_mono_coe _).comp_strict_mono_on $
+  sin_order_iso.symm.strict_mono.strict_mono_on_Icc_extend _
 
 lemma monotone_arcsin : monotone arcsin :=
 (subtype.mono_coe _).comp $ sin_order_iso.symm.monotone.Icc_extend _
 
-lemma inj_on_arcsin : inj_on arcsin (Icc (-1) 1) := strict_mono_incr_on_arcsin.inj_on
+lemma inj_on_arcsin : inj_on arcsin (Icc (-1) 1) := strict_mono_on_arcsin.inj_on
 
 lemma arcsin_inj {x y : ℝ} (hx₁ : -1 ≤ x) (hx₂ : x ≤ 1) (hy₁ : -1 ≤ y) (hy₂ : y ≤ 1) :
   arcsin x = arcsin y ↔ x = y :=
@@ -109,7 +109,7 @@ end
 
 lemma arcsin_le_iff_le_sin {x y : ℝ} (hx : x ∈ Icc (-1 : ℝ) 1) (hy : y ∈ Icc (-(π / 2)) (π / 2)) :
   arcsin x ≤ y ↔ x ≤ sin y :=
-by rw [← arcsin_sin' hy, strict_mono_incr_on_arcsin.le_iff_le hx (sin_mem_Icc _), arcsin_sin' hy]
+by rw [← arcsin_sin' hy, strict_mono_on_arcsin.le_iff_le hx (sin_mem_Icc _), arcsin_sin' hy]
 
 lemma arcsin_le_iff_le_sin' {x y : ℝ} (hy : y ∈ Ico (-(π / 2)) (π / 2)) :
   arcsin x ≤ y ↔ x ≤ sin y :=
@@ -355,10 +355,10 @@ by rw [arccos, cos_pi_div_two_sub, sin_arcsin hx₁ hx₂]
 lemma arccos_cos {x : ℝ} (hx₁ : 0 ≤ x) (hx₂ : x ≤ π) : arccos (cos x) = x :=
 by rw [arccos, ← sin_pi_div_two_sub, arcsin_sin]; simp [sub_eq_add_neg]; linarith
 
-lemma strict_mono_decr_on_arccos : strict_mono_decr_on arccos (Icc (-1) 1) :=
-λ x hx y hy h, sub_lt_sub_left (strict_mono_incr_on_arcsin hx hy h) _
+lemma strict_anti_on_arccos : strict_anti_on arccos (Icc (-1) 1) :=
+λ x hx y hy h, sub_lt_sub_left (strict_mono_on_arcsin hx hy h) _
 
-lemma arccos_inj_on : inj_on arccos (Icc (-1) 1) := strict_mono_decr_on_arccos.inj_on
+lemma arccos_inj_on : inj_on arccos (Icc (-1) 1) := strict_anti_on_arccos.inj_on
 
 lemma arccos_inj {x y : ℝ} (hx₁ : -1 ≤ x) (hx₂ : x ≤ 1) (hy₁ : -1 ≤ y) (hy₂ : y ≤ 1) :
   arccos x = arccos y ↔ x = y :=

src/data/set/function.lean

@@ -795,26 +795,26 @@ by simp
 
 end set
 
-lemma strict_mono_incr_on.inj_on [linear_order α] [preorder β] {f : α → β} {s : set α}
-  (H : strict_mono_incr_on f s) :
+lemma strict_mono_on.inj_on [linear_order α] [preorder β] {f : α → β} {s : set α}
+  (H : strict_mono_on f s) :
   s.inj_on f :=
 λ x hx y hy hxy, show ordering.eq.compares x y, from (H.compares hx hy).1 hxy
 
-lemma strict_mono_decr_on.inj_on [linear_order α] [preorder β] {f : α → β} {s : set α}
-  (H : strict_mono_decr_on f s) :
+lemma strict_anti_on.inj_on [linear_order α] [preorder β] {f : α → β} {s : set α}
+  (H : strict_anti_on f s) :
   s.inj_on f :=
-@strict_mono_incr_on.inj_on α (order_dual β) _ _ f s H
+@strict_mono_on.inj_on α (order_dual β) _ _ f s H
 
-lemma strict_mono_incr_on.comp [preorder α] [preorder β] [preorder γ]
-  {g : β → γ} {f : α → β} {s : set α} {t : set β} (hg : strict_mono_incr_on g t)
-  (hf : strict_mono_incr_on f s) (hs : set.maps_to f s t) :
-  strict_mono_incr_on (g ∘ f) s :=
+lemma strict_mono_on.comp [preorder α] [preorder β] [preorder γ]
+  {g : β → γ} {f : α → β} {s : set α} {t : set β} (hg : strict_mono_on g t)
+  (hf : strict_mono_on f s) (hs : set.maps_to f s t) :
+  strict_mono_on (g ∘ f) s :=
 λ x hx y hy hxy, hg (hs hx) (hs hy) $ hf hx hy hxy
 
-lemma strict_mono.comp_strict_mono_incr_on [preorder α] [preorder β] [preorder γ]
+lemma strict_mono.comp_strict_mono_on [preorder α] [preorder β] [preorder γ]
   {g : β → γ} {f : α → β} {s : set α} (hg : strict_mono g)
-  (hf : strict_mono_incr_on f s) :
-  strict_mono_incr_on (g ∘ f) s :=
+  (hf : strict_mono_on f s) :
+  strict_mono_on (g ∘ f) s :=
 λ x hx y hy hxy, hg $ hf hx hy hxy
 
 lemma strict_mono.cod_restrict [preorder α] [preorder β] {f : α → β} (hf : strict_mono f)

src/data/set/intervals/proj_Icc.lean

@@ -60,7 +60,7 @@ lemma proj_Icc_surjective : surjective (proj_Icc a b h) :=
 lemma monotone_proj_Icc : monotone (proj_Icc a b h) :=
 λ x y hxy, max_le_max le_rfl $ min_le_min le_rfl hxy
 
-lemma strict_mono_incr_on_proj_Icc : strict_mono_incr_on (proj_Icc a b h) (Icc a b) :=
+lemma strict_mono_on_proj_Icc : strict_mono_on (proj_Icc a b h) (Icc a b) :=
 λ x hx y hy hxy, by simpa only [proj_Icc_of_mem, hx, hy]
 
 /-- Extend a function `[a, b] → β` to a map `α → β`. -/
@@ -104,6 +104,6 @@ variables [preorder β] {a b : α} (h : a ≤ b) {f : Icc a b → β}
 lemma monotone.Icc_extend (hf : monotone f) : monotone (Icc_extend h f) :=
 hf.comp $ monotone_proj_Icc h
 
-lemma strict_mono.strict_mono_incr_on_Icc_extend (hf : strict_mono f) :
-  strict_mono_incr_on (Icc_extend h f) (Icc a b) :=
-hf.comp_strict_mono_incr_on (strict_mono_incr_on_proj_Icc h)
+lemma strict_mono.strict_mono_on_Icc_extend (hf : strict_mono f) :
+  strict_mono_on (Icc_extend h f) (Icc a b) :=
+hf.comp_strict_mono_on (strict_mono_on_proj_Icc h)