doc(order/*): use "monotone" / "antitone" in place of "monotonically …

…increasing" / "monotonically decreasing" (#9408)

This PR cleans up the references to monotone and antitone function in lemmas and docstrings.

It doesn't touch anything beyond the docstrings.



Co-authored-by: Oliver Nash <github@olivernash.org>

docs/undergrad.yaml

@@ -308,7 +308,7 @@ Single Variable Real Analysis:
     limits: 'filter.tendsto'
     intermediate value theorem: 'intermediate_value_Icc'
     image of a segment: 'real.image_Icc'
-    continuity of monotonic functions: 'order_iso.continuous'
+    continuity of monotone functions: 'order_iso.continuous'
     continuity of inverse functions: 'order_iso.to_homeomorph'
   Differentiability:
     derivative at a point: 'has_deriv_at'

src/algebra/continued_fractions/computation/approximations.lean

@@ -297,7 +297,7 @@ begin
   exact (le_of_succ_succ_nth_continuants_aux_b nth_part_denom_eq)
 end
 
-/-- Shows that the sequence of denominators is monotonically increasing, that is `Bₙ ≤ Bₙ₊₁`. -/
+/-- Shows that the sequence of denominators is monotone, that is `Bₙ ≤ Bₙ₊₁`. -/
 theorem of_denom_mono : (gcf.of v).denominators n ≤ (gcf.of v).denominators (n + 1) :=
 begin
   let g := gcf.of v,

src/algebra/continued_fractions/computation/terminates_iff_rat.lean

@@ -265,7 +265,7 @@ lemma of_inv_fr_num_lt_num_of_pos (q_pos : 0 < q) :
 rat.fract_inv_num_lt_num_of_pos q_pos
 
 /-- Shows that the sequence of numerators of the fractional parts of the stream is strictly
-monotonically decreasing. -/
+antitone. -/
 lemma stream_succ_nth_fr_num_lt_nth_fr_num_rat {ifp_n ifp_succ_n : int_fract_pair ℚ}
   (stream_nth_eq : int_fract_pair.stream q n = some ifp_n)
   (stream_succ_nth_eq : int_fract_pair.stream q (n + 1) = some ifp_succ_n) :

src/analysis/calculus/mean_value.lean

@@ -52,7 +52,7 @@ In this file we prove the following facts:
 * `convex.mono_of_deriv_nonneg`, `convex.antitone_of_deriv_nonpos`,
   `convex.strict_mono_of_deriv_pos`, `convex.strict_antitone_of_deriv_neg` :
   if the derivative of a function is non-negative/non-positive/positive/negative, then
-  the function is monotone/monotonically decreasing/strictly monotone/strictly monotonically
+  the function is monotone/antitone/strictly monotone/strictly monotonically
   decreasing.
 
 * `convex_on_of_deriv_mono`, `convex_on_of_deriv2_nonneg` : if the derivative of a function
@@ -904,15 +904,15 @@ convex_univ.image_sub_le_mul_sub_of_deriv_le hf.continuous.continuous_on hf.diff
 
 /-- Let `f` be a function continuous on a convex (or, equivalently, connected) subset `D`
 of the real line. If `f` is differentiable on the interior of `D` and `f'` is positive, then
-`f` is a strictly monotonically increasing function on `D`. -/
+`f` is a strictly monotone function on `D`. -/
 theorem convex.strict_mono_of_deriv_pos {D : set ℝ} (hD : convex ℝ D) {f : ℝ → ℝ}
   (hf : continuous_on f D) (hf' : differentiable_on ℝ f (interior D))
   (hf'_pos : ∀ x ∈ interior D, 0 < deriv f x) :
   ∀ x y ∈ D, x < y → f x < f y :=
 by simpa only [zero_mul, sub_pos] using hD.mul_sub_lt_image_sub_of_lt_deriv hf hf' hf'_pos
 
 /-- Let `f : ℝ → ℝ` be a differentiable function. If `f'` is positive, then
-`f` is a strictly monotonically increasing function. -/
+`f` is a strictly monotone function. -/
 theorem strict_mono_of_deriv_pos {f : ℝ → ℝ} (hf : differentiable ℝ f)
   (hf'_pos : ∀ x, 0 < deriv f x) :
   strict_mono f :=
@@ -921,31 +921,31 @@ theorem strict_mono_of_deriv_pos {f : ℝ → ℝ} (hf : differentiable ℝ f)
 
 /-- Let `f` be a function continuous on a convex (or, equivalently, connected) subset `D`
 of the real line. If `f` is differentiable on the interior of `D` and `f'` is nonnegative, then
-`f` is a monotonically increasing function on `D`. -/
+`f` is a monotone function on `D`. -/
 theorem convex.mono_of_deriv_nonneg {D : set ℝ} (hD : convex ℝ D) {f : ℝ → ℝ}
   (hf : continuous_on f D) (hf' : differentiable_on ℝ f (interior D))
   (hf'_nonneg : ∀ x ∈ interior D, 0 ≤ deriv f x) :
   ∀ x y ∈ D, x ≤ y → f x ≤ f y :=
 by simpa only [zero_mul, sub_nonneg] using hD.mul_sub_le_image_sub_of_le_deriv hf hf' hf'_nonneg
 
 /-- Let `f : ℝ → ℝ` be a differentiable function. If `f'` is nonnegative, then
-`f` is a monotonically increasing function. -/
+`f` is a monotone function. -/
 theorem mono_of_deriv_nonneg {f : ℝ → ℝ} (hf : differentiable ℝ f) (hf' : ∀ x, 0 ≤ deriv f x) :
   monotone f :=
 λ x y hxy, convex_univ.mono_of_deriv_nonneg hf.continuous.continuous_on hf.differentiable_on
   (λ x _, hf' x) x y trivial trivial hxy
 
 /-- Let `f` be a function continuous on a convex (or, equivalently, connected) subset `D`
 of the real line. If `f` is differentiable on the interior of `D` and `f'` is negative, then
-`f` is a strictly monotonically decreasing function on `D`. -/
+`f` is a strictly antitone function on `D`. -/
 theorem convex.strict_antitone_of_deriv_neg {D : set ℝ} (hD : convex ℝ D) {f : ℝ → ℝ}
   (hf : continuous_on f D) (hf' : differentiable_on ℝ f (interior D))
   (hf'_neg : ∀ x ∈ interior D, deriv f x < 0) :
   ∀ x y ∈ D, x < y → f y < f x :=
 by simpa only [zero_mul, sub_lt_zero] using hD.image_sub_lt_mul_sub_of_deriv_lt hf hf' hf'_neg
 
 /-- Let `f : ℝ → ℝ` be a differentiable function. If `f'` is negative, then
-`f` is a strictly monotonically decreasing function. -/
+`f` is a strictly antitone function. -/
 theorem strict_antitone_of_deriv_neg {f : ℝ → ℝ} (hf : differentiable ℝ f)
   (hf' : ∀ x, deriv f x < 0) :
   ∀ ⦃x y⦄, x < y → f y < f x :=
@@ -954,15 +954,15 @@ theorem strict_antitone_of_deriv_neg {f : ℝ → ℝ} (hf : differentiable ℝ
 
 /-- Let `f` be a function continuous on a convex (or, equivalently, connected) subset `D`
 of the real line. If `f` is differentiable on the interior of `D` and `f'` is nonpositive, then
-`f` is a monotonically decreasing function on `D`. -/
+`f` is an antitone function on `D`. -/
 theorem convex.antitone_of_deriv_nonpos {D : set ℝ} (hD : convex ℝ D) {f : ℝ → ℝ}
   (hf : continuous_on f D) (hf' : differentiable_on ℝ f (interior D))
   (hf'_nonpos : ∀ x ∈ interior D, deriv f x ≤ 0) :
   ∀ x y ∈ D, x ≤ y → f y ≤ f x :=
 by simpa only [zero_mul, sub_nonpos] using hD.image_sub_le_mul_sub_of_deriv_le hf hf' hf'_nonpos
 
 /-- Let `f : ℝ → ℝ` be a differentiable function. If `f'` is nonpositive, then
-`f` is a monotonically decreasing function. -/
+`f` is an antitone function. -/
 theorem antitone_of_deriv_nonpos {f : ℝ → ℝ} (hf : differentiable ℝ f) (hf' : ∀ x, deriv f x ≤ 0) :
   ∀ ⦃x y⦄, x ≤ y → f y ≤ f x :=
 λ x y hxy, convex_univ.antitone_of_deriv_nonpos hf.continuous.continuous_on hf.differentiable_on
@@ -995,7 +995,7 @@ begin
 end
 
 /-- If a function `f` is continuous on a convex set `D ⊆ ℝ`, is differentiable on its interior,
-and `f'` is antimonotone on the interior, then `f` is concave on `D`. -/
+and `f'` is antitone on the interior, then `f` is concave on `D`. -/
 theorem concave_on_of_deriv_antitone {D : set ℝ} (hD : convex ℝ D) {f : ℝ → ℝ}
   (hf : continuous_on f D) (hf' : differentiable_on ℝ f (interior D))
   (hf'_mono : ∀ x y ∈ interior D, x ≤ y → deriv f y ≤ deriv f x) :
@@ -1014,7 +1014,7 @@ theorem convex_on_univ_of_deriv_mono {f : ℝ → ℝ} (hf : differentiable ℝ
 convex_on_of_deriv_mono convex_univ hf.continuous.continuous_on hf.differentiable_on
   (λ x y _ _ h, hf'_mono h)
 
-/-- If a function `f` is differentiable and `f'` is antimonotone on `ℝ` then `f` is concave. -/
+/-- If a function `f` is differentiable and `f'` is antitone on `ℝ` then `f` is concave. -/
 theorem concave_on_univ_of_deriv_antitone {f : ℝ → ℝ} (hf : differentiable ℝ f)
   (hf'_antitone : ∀⦃a b⦄, a ≤ b → (deriv f) b ≤ (deriv f) a) : concave_on ℝ univ f :=
 concave_on_of_deriv_antitone convex_univ hf.continuous.continuous_on hf.differentiable_on

src/analysis/p_series.lean

@@ -158,7 +158,7 @@ if and only if `1 < p`. -/
 @[simp] lemma real.summable_nat_rpow_inv {p : ℝ} : summable (λ n, (n ^ p)⁻¹ : ℕ → ℝ) ↔ 1 < p :=
 begin
   cases le_or_lt 0 p with hp hp,
-  /- Cauchy condensation test applies only to monotonically decreasing sequences, so we consider the
+  /- Cauchy condensation test applies only to antitone sequences, so we consider the
   cases `0 ≤ p` and `p < 0` separately. -/
   { rw ← summable_condensed_iff_of_nonneg,
     { simp_rw [nat.cast_pow, nat.cast_two, ← rpow_nat_cast, ← rpow_mul zero_lt_two.le, mul_comm _ p,

src/data/ordmap/ordnode.lean

@@ -482,7 +482,7 @@ def partition (p : α → Prop) [decidable_pred p] : ordnode α → ordnode α 
   else (merge l₁ r₁, link l₂ x r₂)
 
 /-- O(n). Map a function across a tree, without changing the structure. Only valid when
-the function is strictly monotonic, i.e. `x < y → f x < f y`.
+the function is strictly monotone, i.e. `x < y → f x < f y`.
 
      partition (λ x, x + 2) {1, 2, 4} = {2, 3, 6}
      partition (λ x : ℕ, x - 2) {1, 2, 4} = precondition violation -/

src/measure_theory/measure/hausdorff.lean

@@ -71,7 +71,7 @@ measures.
   on an extended metric space `X` (that is, it is additive on pairs of metric separated sets), then
   every Borel set is Caratheodory measurable (hence, `μ` defines an actual
   `measure_theory.measure`). See also `measure_theory.measure.mk_metric`.
-* `measure_theory.measure.hausdorff_measure_mono`: `μH[d] s` is a monotonically decreasing function
+* `measure_theory.measure.hausdorff_measure_mono`: `μH[d] s` is an antitone function
   of `d`.
 * `measure_theory.measure.hausdorff_measure_zero_or_top`: if `d₁ < d₂`, then for any `s`, either
   `μH[d₂] s = 0` or `μH[d₁] s = ∞`. Together with the previous lemma, this means that `μH[d] s` is

src/measure_theory/measure/stieltjes.lean

@@ -91,8 +91,8 @@ instance : inhabited stieltjes_function := ⟨stieltjes_function.id⟩
 
 /-! ### The outer measure associated to a Stieltjes function -/
 
-/-- Length of an interval. This is the largest monotonic function which correctly
-  measures all intervals. -/
+/-- Length of an interval. This is the largest monotone function which correctly measures all
+intervals. -/
 def length (s : set ℝ) : ℝ≥0∞ := ⨅a b (h : s ⊆ Ioc a b), of_real (f b - f a)
 
 @[simp] lemma length_empty : f.length ∅ = 0 :=

src/order/conditionally_complete_lattice.lean

@@ -502,9 +502,8 @@ theorem cinfi_eq_of_forall_ge_of_forall_gt_exists_lt [nonempty ι] {f : ι → 
   (h₂ : ∀ w, b < w → (∃ i, f i < w)) : (⨅ (i : ι), f i) = b :=
 @csupr_eq_of_forall_le_of_forall_lt_exists_gt (order_dual α) _ _ _ _ ‹_› ‹_› ‹_›
 
-/-- Nested intervals lemma: if `f` is a monotonically increasing sequence, `g` is a monotonically
-decreasing sequence, and `f n ≤ g n` for all `n`, then `⨆ n, f n` belongs to all the intervals
-`[f n, g n]`. -/
+/-- Nested intervals lemma: if `f` is a monotone sequence, `g` is an antitone sequence, and
+`f n ≤ g n` for all `n`, then `⨆ n, f n` belongs to all the intervals `[f n, g n]`. -/
 lemma csupr_mem_Inter_Icc_of_mono_incr_of_mono_decr [nonempty β] [semilattice_sup β]
   {f g : β → α} (hf : monotone f) (hg : ∀ ⦃m n⦄, m ≤ n → g n ≤ g m) (h : ∀ n, f n ≤ g n) :
   (⨆ n, f n) ∈ ⋂ n, Icc (f n) (g n) :=
@@ -514,15 +513,15 @@ begin
     csupr_le $ λ m, _⟩); exact forall_le_of_monotone_of_mono_decr hf hg h _ _
 end
 
-/-- Nested intervals lemma: if `[f n, g n]` is a monotonically decreasing sequence of nonempty
+/-- Nested intervals lemma: if `[f n, g n]` is an antitone sequence of nonempty
 closed intervals, then `⨆ n, f n` belongs to all the intervals `[f n, g n]`. -/
 lemma csupr_mem_Inter_Icc_of_mono_decr_Icc [nonempty β] [semilattice_sup β]
   {f g : β → α} (h : ∀ ⦃m n⦄, m ≤ n → Icc (f n) (g n) ⊆ Icc (f m) (g m)) (h' : ∀ n, f n ≤ g n) :
   (⨆ n, f n) ∈ ⋂ n, Icc (f n) (g n) :=
 csupr_mem_Inter_Icc_of_mono_incr_of_mono_decr (λ m n hmn, ((Icc_subset_Icc_iff (h' n)).1 (h hmn)).1)
   (λ m n hmn, ((Icc_subset_Icc_iff (h' n)).1 (h hmn)).2) h'
 
-/-- Nested intervals lemma: if `[f n, g n]` is a monotonically decreasing sequence of nonempty
+/-- Nested intervals lemma: if `[f n, g n]` is an antitone sequence of nonempty
 closed intervals, then `⨆ n, f n` belongs to all the intervals `[f n, g n]`. -/
 lemma csupr_mem_Inter_Icc_of_mono_decr_Icc_nat
   {f g : ℕ → α} (h : ∀ n, Icc (f (n + 1)) (g (n + 1)) ⊆ Icc (f n) (g n)) (h' : ∀ n, f n ≤ g n) :

src/order/directed.lean

@@ -69,7 +69,7 @@ lemma monotone.directed_le [semilattice_sup α] [preorder β] {f : α → β} :
   monotone f → directed (≤) f :=
 directed_of_sup
 
-/-- An antimonotone function on an inf-semilattice is directed. -/
+/-- An antitone function on an inf-semilattice is directed. -/
 lemma directed_of_inf [semilattice_inf α] {r : β → β → Prop} {f : α → β}
   (hf : ∀ a₁ a₂, a₁ ≤ a₂ → r (f a₂) (f a₁)) : directed r f :=
 λ x y, ⟨x ⊓ y, hf _ _ inf_le_left, hf _ _ inf_le_right⟩

src/order/filter/bases.lean

@@ -49,7 +49,7 @@ and consequences are derived.
 * `has_basis.tendsto_right_iff`, `has_basis.tendsto_left_iff`, `has_basis.tendsto_iff` : restate
   `tendsto f l l'` in terms of bases.
 * `is_countably_generated_iff_exists_antitone_basis` : proves a filter is
-  countably generated if and only if it admis a basis parametrized by a
+  countably generated if and only if it admits a basis parametrized by a
   decreasing sequence of sets indexed by `ℕ`.
 * `tendsto_iff_seq_tendsto ` : an abstract version of "sequentially continuous implies continuous".
 
@@ -597,7 +597,7 @@ structure is_antitone_basis extends is_basis p'' s'' : Prop :=
 (decreasing : ∀ {i j}, p'' i → p'' j → i ≤ j → s'' j ⊆ s'' i)
 (mono : monotone p'')
 
-/-- We say that a filter `l` has a antitone basis `s : ι → set α` bounded by `p : ι → Prop`,
+/-- We say that a filter `l` has an antitone basis `s : ι → set α` bounded by `p : ι → Prop`,
 if `t ∈ l` if and only if `t` includes `s i` for some `i` such that `p i`,
 and `s` is decreasing and `p` is increasing, ie `i ≤ j → p i → p j`. -/
 structure has_antitone_basis (l : filter α) (p : ι'' → Prop) (s : ι'' → set α)
@@ -813,8 +813,7 @@ begin
       this.to_has_basis.mem_iff.2 ⟨i, trivial, x_subset i⟩))
 end
 
-/-- A countably generated filter admits a basis formed by a monotonically decreasing sequence of
-sets. -/
+/-- A countably generated filter admits a basis formed by an antitone sequence of sets. -/
 lemma exists_antitone_basis {f : filter α} (cblb : f.is_countably_generated) :
   ∃ x : ℕ → set α, f.has_antitone_basis (λ _, true) x :=
 let ⟨x, hxf, hx⟩ := cblb.exists_antitone_subbasis f.basis_sets in ⟨x, hx⟩

src/order/filter/extr.lean

@@ -32,7 +32,7 @@ Similar predicates with `_on` suffix are particular cases for `l = 𝓟 s`.
 
 * `is_*_*.comp_mono` : if `x` is an extremum for `f` and `g` is a monotone function,
   then `x` is an extremum for `g ∘ f`;
-* `is_*_*.comp_antitone` : similarly for the case of monotonically decreasing `g`;
+* `is_*_*.comp_antitone` : similarly for the case of antitone `g`;
 * `is_*_*.bicomp_mono` : if `x` is an extremum of the same type for `f` and `g`
   and a binary operation `op` is monotone in both arguments, then `x` is an extremum
   of the same type for `λ x, op (f x) (g x)`.

src/order/lattice.lean

@@ -239,8 +239,8 @@ suffices (∃b, ¬b ≤ a) → (∃b, a < b),
 assume ⟨b, hb⟩,
 ⟨a ⊔ b, lt_of_le_of_ne le_sup_left $ mt left_eq_sup.1 hb⟩
 
-/-- If `f` is a monotonically increasing sequence, `g` is a monotonically decreasing
-sequence, and `f n ≤ g n` for all `n`, then for all `m`, `n` we have `f m ≤ g n`. -/
+/-- If `f` is monotone, `g` is antitone, and `f a ≤ g a` for all `a`, then for all `a`, `b` we have
+`f a ≤ g b`. -/
 theorem forall_le_of_monotone_of_mono_decr {β : Type*} [preorder β]
   {f g : α → β} (hf : monotone f) (hg : ∀ ⦃m n⦄, m ≤ n → g n ≤ g m)
   (h : ∀ n, f n ≤ g n) (m n : α) : f m ≤ g n :=

src/order/omega_complete_partial_order.lean

@@ -117,7 +117,7 @@ end preorder_hom
 
 namespace omega_complete_partial_order
 
-/-- A chain is a monotonically increasing sequence.
+/-- A chain is a monotone sequence.
 
 See the definition on page 114 of [gunter1992]. -/
 def chain (α : Type u) [preorder α] :=

src/order/order_iso_nat.lean

@@ -170,14 +170,14 @@ begin
     exact n.succ_ne_self.symm (rel_embedding.to_preorder_hom_injective _ (hn _ n.le_succ)), },
 end
 
-/-- Given an eventually-constant monotonic sequence `a₀ ≤ a₁ ≤ a₂ ≤ ...` in a partially-ordered
+/-- Given an eventually-constant monotone sequence `a₀ ≤ a₁ ≤ a₂ ≤ ...` in a partially-ordered
 type, `monotonic_sequence_limit_index a` is the least natural number `n` for which `aₙ` reaches the
 constant value. For sequences that are not eventually constant, `monotonic_sequence_limit_index a`
 is defined, but is a junk value. -/
 noncomputable def monotonic_sequence_limit_index {α : Type*} [partial_order α] (a : ℕ →ₘ α) : ℕ :=
 Inf { n | ∀ m, n ≤ m → a n = a m }
 
-/-- The constant value of an eventually-constant monotonic sequence `a₀ ≤ a₁ ≤ a₂ ≤ ...` in a
+/-- The constant value of an eventually-constant monotone sequence `a₀ ≤ a₁ ≤ a₂ ≤ ...` in a
 partially-ordered type. -/
 noncomputable def monotonic_sequence_limit {α : Type*} [partial_order α] (a : ℕ →ₘ α) :=
 a (monotonic_sequence_limit_index a)