chore(order/*): Change order_hom notation (#10988)

This changes the notation for `order_hom` from `α →ₘ β` to `α →o β` to match `order_embedding` and `order_iso`, which are respectively `α ↪o β` and `α ≃o β`. This also solves the conflict with measurable functions.

src/algebra/lie/solvable.lean

@@ -101,7 +101,7 @@ derived_series_of_ideal_le (le_refl I) h
 lemma derived_series_of_ideal_add_le_add (J : lie_ideal R L) (k l : ℕ) :
   D (k + l) (I + J) ≤ (D k I) + (D l J) :=
 begin
-  let D₁ : lie_ideal R L →ₘ lie_ideal R L :=
+  let D₁ : lie_ideal R L →o lie_ideal R L :=
   { to_fun    := λ I, ⁅I, I⁆,
     monotone' := λ I J h, lie_submodule.mono_lie I J I J h h, },
   have h₁ : ∀ (I J : lie_ideal R L), D₁ (I ⊔ J) ≤ (D₁ I) ⊔ J,

src/algebraic_topology/simplex_category.lean

@@ -63,20 +63,20 @@ def len (n : simplex_category.{u}) : ℕ := n.down
 /-- Morphisms in the simplex_category. -/
 @[irreducible, nolint has_inhabited_instance]
 protected def hom (a b : simplex_category.{u}) : Type u :=
-ulift (fin (a.len + 1) →ₘ fin (b.len + 1))
+ulift (fin (a.len + 1) →o fin (b.len + 1))
 
 namespace hom
 
 local attribute [semireducible] simplex_category.hom
 
 /-- Make a moprhism in `simplex_category` from a monotone map of fin's. -/
-def mk {a b : simplex_category.{u}} (f : fin (a.len + 1) →ₘ fin (b.len + 1)) :
+def mk {a b : simplex_category.{u}} (f : fin (a.len + 1) →o fin (b.len + 1)) :
   simplex_category.hom a b :=
 ulift.up f
 
 /-- Recover the monotone map from a morphism in the simplex category. -/
 def to_order_hom {a b : simplex_category.{u}} (f : simplex_category.hom a b) :
-  fin (a.len + 1) →ₘ fin (b.len + 1) :=
+  fin (a.len + 1) →o fin (b.len + 1) :=
 ulift.down f
 
 @[ext] lemma ext {a b : simplex_category.{u}} (f g : simplex_category.hom a b) :
@@ -87,11 +87,11 @@ ulift.down f
 by {cases f, refl}
 
 @[simp] lemma to_order_hom_mk {a b : simplex_category.{u}}
-  (f : fin (a.len + 1) →ₘ fin (b.len + 1)) : (mk f).to_order_hom = f :=
+  (f : fin (a.len + 1) →o fin (b.len + 1)) : (mk f).to_order_hom = f :=
 by simp [to_order_hom, mk]
 
 lemma mk_to_order_hom_apply {a b : simplex_category.{u}}
-  (f : fin (a.len + 1) →ₘ fin (b.len + 1)) (i : fin (a.len + 1)) :
+  (f : fin (a.len + 1) →o fin (b.len + 1)) (i : fin (a.len + 1)) :
   (mk f).to_order_hom i = f i := rfl
 
 /-- Identity morphisms of `simplex_category`. -/
@@ -128,7 +128,7 @@ This is useful for constructing morphisms beetween `[n]` directly
 without identifying `n` with `[n].len`.
 -/
 @[simp]
-def mk_hom {n m : ℕ} (f : (fin (n+1)) →ₘ (fin (m+1))) : [n] ⟶ [m] :=
+def mk_hom {n m : ℕ} (f : (fin (n+1)) →o (fin (m+1))) : [n] ⟶ [m] :=
 simplex_category.hom.mk f
 
 lemma hom_zero_zero (f : [0] ⟶ [0]) : f = 𝟙 _ :=

src/combinatorics/additive/salem_spencer.lean

@@ -233,7 +233,7 @@ Salem-Spencer subset. -/
 @[to_additive "The additive Roth number of a finset is the cardinality of its biggest additive
 Salem-Spencer subset. The usual Roth number corresponds to `roth_number (finset.range n)`, see
 `roth_number_nat`. "]
-def mul_roth_number : finset α →ₘ ℕ :=
+def mul_roth_number : finset α →o ℕ :=
 ⟨λ s, nat.find_greatest (λ m, ∃ t ⊆ s, t.card = m ∧ mul_salem_spencer (t : set α)) s.card,
 begin
   rintro t u htu,
@@ -352,7 +352,7 @@ Trivially, `roth_number N ≤ N`, but Roth's theorem (proved in 1953) shows that
 `N * exp(-C sqrt(log(N))) ≤ roth_number N`.
 A significant refinement of Roth's theorem by Bloom and Sisask announced in 2020 gives
 `roth_number N = O(N / (log N)^(1+c))` for an absolute constant `c`. -/
-def roth_number_nat : ℕ →ₘ ℕ :=
+def roth_number_nat : ℕ →o ℕ :=
 ⟨λ n, add_roth_number (range n), add_roth_number.mono.comp range_mono⟩
 
 lemma roth_number_nat_def (n : ℕ) : roth_number_nat n = add_roth_number (range n) := rfl

src/control/lawful_fix.lean

@@ -34,7 +34,7 @@ halting problem. Instead, this requirement is limited to only functions that are
 sense of `ω`-complete partial orders, which excludes the example because it is not monotone
 (making the input argument less defined can make `f` more defined). -/
 class lawful_fix (α : Type*) [omega_complete_partial_order α] extends has_fix α :=
-(fix_eq : ∀ {f : α →ₘ α}, continuous f → has_fix.fix f = f (has_fix.fix f))
+(fix_eq : ∀ {f : α →o α}, continuous f → has_fix.fix f = f (has_fix.fix f))
 
 lemma lawful_fix.fix_eq' {α} [omega_complete_partial_order α] [lawful_fix α]
   {f : α → α} (hf : continuous' f) :
@@ -47,7 +47,7 @@ open part nat nat.upto
 
 namespace fix
 
-variables (f : (Π a, part $ β a) →ₘ (Π a, part $ β a))
+variables (f : (Π a, part $ β a) →o (Π a, part $ β a))
 
 lemma approx_mono' {i : ℕ} : fix.approx f i ≤ fix.approx f (succ i) :=
 begin
@@ -122,7 +122,7 @@ end fix
 open fix
 
 variables {α}
-variables (f : (Π a, part $ β a) →ₘ (Π a, part $ β a))
+variables (f : (Π a, part $ β a) →o (Π a, part $ β a))
 
 open omega_complete_partial_order
 
@@ -173,11 +173,11 @@ namespace part
 
 /-- `to_unit` as a monotone function -/
 @[simps]
-def to_unit_mono (f : part α →ₘ part α) : (unit → part α) →ₘ (unit → part α) :=
+def to_unit_mono (f : part α →o part α) : (unit → part α) →o (unit → part α) :=
 { to_fun := λ x u, f (x u),
   monotone' := λ x y (h : x ≤ y) u, f.monotone $ h u }
 
-lemma to_unit_cont (f : part α →ₘ part α) (hc : continuous f) : continuous (to_unit_mono f)
+lemma to_unit_cont (f : part α →o part α) (hc : continuous f) : continuous (to_unit_mono f)
 | c := begin
   ext ⟨⟩ : 1,
   dsimp [omega_complete_partial_order.ωSup],
@@ -204,14 +204,14 @@ variables (α β γ)
 /-- `sigma.curry` as a monotone function. -/
 @[simps]
 def monotone_curry [∀ x y, preorder $ γ x y] :
-  (Π x : Σ a, β a, γ x.1 x.2) →ₘ (Π a (b : β a), γ a b) :=
+  (Π x : Σ a, β a, γ x.1 x.2) →o (Π a (b : β a), γ a b) :=
 { to_fun := curry,
   monotone' := λ x y h a b, h ⟨a,b⟩ }
 
 /-- `sigma.uncurry` as a monotone function. -/
 @[simps]
 def monotone_uncurry [∀ x y, preorder $ γ x y] :
-  (Π a (b : β a), γ a b) →ₘ (Π x : Σ a, β a, γ x.1 x.2) :=
+  (Π a (b : β a), γ a b) →o (Π x : Σ a, β a, γ x.1 x.2) :=
 { to_fun := uncurry,
   monotone' := λ x y h a, h a.1 a.2 }
 
@@ -236,7 +236,7 @@ variables [∀ x y, omega_complete_partial_order $ γ x y]
 
 section curry
 
-variables {f : (Π x (y : β x), γ x y) →ₘ (Π x (y : β x), γ x y)}
+variables {f : (Π x (y : β x), γ x y) →o (Π x (y : β x), γ x y)}
 variables (hc : continuous f)
 
 lemma uncurry_curry_continuous :

src/data/finset/option.lean

@@ -69,7 +69,7 @@ by simp [insert_none]
 
 /-- Given `s : finset (option α)`, `s.erase_none : finset α` is the set of `x : α` such that
 `some x ∈ s`. -/
-def erase_none : finset (option α) →ₘ finset α :=
+def erase_none : finset (option α) →o finset α :=
 (finset.map_embedding (equiv.option_is_some_equiv α).to_embedding).to_order_hom.comp
   ⟨finset.subtype _, subtype_mono⟩
 

src/linear_algebra/basic.lean

@@ -983,7 +983,7 @@ begin
   simp only [Sup_eq_supr', mem_supr_of_directed _ hdir.directed_coe, set_coe.exists, subtype.coe_mk]
 end
 
-@[norm_cast, simp] lemma coe_supr_of_chain (a : ℕ →ₘ submodule R M) :
+@[norm_cast, simp] lemma coe_supr_of_chain (a : ℕ →o submodule R M) :
   (↑(⨆ k, a k) : set M) = ⋃ k, (a k : set M) :=
 coe_supr_of_directed a a.monotone.directed_le
 
@@ -993,7 +993,7 @@ lemma coe_scott_continuous : omega_complete_partial_order.continuous'
   (coe : submodule R M → set M) :=
 ⟨set_like.coe_mono, coe_supr_of_chain⟩
 
-@[simp] lemma mem_supr_of_chain (a : ℕ →ₘ submodule R M) (m : M) :
+@[simp] lemma mem_supr_of_chain (a : ℕ →o submodule R M) (m : M) :
   m ∈ (⨆ k, a k) ↔ ∃ k, m ∈ a k :=
 mem_supr_of_directed a a.monotone.directed_le
 
@@ -1493,7 +1493,7 @@ end
 The decreasing sequence of submodules consisting of the ranges of the iterates of a linear map.
 -/
 @[simps]
-def iterate_range (f : M →ₗ[R] M) : ℕ →ₘ order_dual (submodule R M) :=
+def iterate_range (f : M →ₗ[R] M) : ℕ →o order_dual (submodule R M) :=
 ⟨λ n, (f ^ n).range, λ n m w x h, begin
   obtain ⟨c, rfl⟩ := le_iff_exists_add.mp w,
   rw linear_map.mem_range at h,
@@ -1634,7 +1634,7 @@ end
 The increasing sequence of submodules consisting of the kernels of the iterates of a linear map.
 -/
 @[simps]
-def iterate_ker (f : M →ₗ[R] M) : ℕ →ₘ submodule R M :=
+def iterate_ker (f : M →ₗ[R] M) : ℕ →o submodule R M :=
 ⟨λ n, (f ^ n).ker, λ n m w x h, begin
   obtain ⟨c, rfl⟩ := le_iff_exists_add.mp w,
   rw linear_map.mem_ker at h,

src/linear_algebra/eigenspace.lean

@@ -332,7 +332,7 @@ complete_lattice.independent.linear_independent _
 /-- The generalized eigenspace for a linear map `f`, a scalar `μ`, and an exponent `k ∈ ℕ` is the
 kernel of `(f - μ • id) ^ k`. (Def 8.10 of [axler2015]). Furthermore, a generalized eigenspace for
 some exponent `k` is contained in the generalized eigenspace for exponents larger than `k`. -/
-def generalized_eigenspace (f : End R M) (μ : R) : ℕ →ₘ submodule R M :=
+def generalized_eigenspace (f : End R M) (μ : R) : ℕ →o submodule R M :=
 { to_fun    := λ k, ((f - algebra_map R (End R M) μ) ^ k).ker,
   monotone' := λ k m hm,
   begin

src/linear_algebra/prod.lean

@@ -588,7 +588,7 @@ noncomputable def tunnel' (f : M × N →ₗ[R] M) (i : injective f) :
 Give an injective map `f : M × N →ₗ[R] M` we can find a nested sequence of submodules
 all isomorphic to `M`.
 -/
-def tunnel (f : M × N →ₗ[R] M) (i : injective f) : ℕ →ₘ order_dual (submodule R M) :=
+def tunnel (f : M × N →ₗ[R] M) (i : injective f) : ℕ →o order_dual (submodule R M) :=
 ⟨λ n, (tunnel' f i n).1, monotone_nat_of_le_succ (λ n, begin
     dsimp [tunnel', tunnel_aux],
     rw [submodule.map_comp, submodule.map_comp],

src/order/closure.lean

@@ -54,7 +54,7 @@ variable (α : Type*)
 
 /-- A closure operator on the preorder `α` is a monotone function which is extensive (every `x`
 is less than its closure) and idempotent. -/
-structure closure_operator [preorder α] extends α →ₘ α :=
+structure closure_operator [preorder α] extends α →o α :=
 (le_closure' : ∀ x, x ≤ to_fun x)
 (idempotent' : ∀ x, to_fun (to_fun x) = to_fun x)
 

src/order/fixed_points.lean

@@ -36,15 +36,15 @@ namespace order_hom
 
 section basic
 
-variables [complete_lattice α] (f : α →ₘ α)
+variables [complete_lattice α] (f : α →o α)
 
 /-- Least fixed point of a monotone function -/
-def lfp : (α →ₘ α) →ₘ α :=
+def lfp : (α →o α) →o α :=
 { to_fun := λ f, Inf {a | f a ≤ a},
   monotone' := λ f g hle, Inf_le_Inf $ λ a ha, (hle a).trans ha }
 
 /-- Greatest fixed point of a monotone function -/
-def gfp : (α →ₘ α) →ₘ α :=
+def gfp : (α →o α) →o α :=
 { to_fun := λ f, Sup {a | a ≤ f a},
   monotone' := λ f g hle, Sup_le_Sup $ λ a ha, le_trans ha (hle a) }
 
@@ -114,7 +114,7 @@ end basic
 
 section eqn
 
-variables [complete_lattice α] [complete_lattice β] (f : β →ₘ α) (g : α →ₘ β)
+variables [complete_lattice α] [complete_lattice β] (f : β →o α) (g : α →o β)
 
 -- Rolling rule
 lemma map_lfp_comp : f (lfp (g.comp f)) = lfp (f.comp g) :=
@@ -125,7 +125,7 @@ lemma map_gfp_comp : f ((g.comp f).gfp) = (f.comp g).gfp :=
 f.dual.map_lfp_comp g.dual
 
 -- Diagonal rule
-lemma lfp_lfp (h : α →ₘ α →ₘ α) :
+lemma lfp_lfp (h : α →o α →o α) :
   lfp (lfp.comp h) = lfp h.on_diag :=
 begin
   let a := lfp (lfp.comp h),
@@ -137,15 +137,15 @@ begin
          ... = a               : ha
 end
 
-lemma gfp_gfp (h : α →ₘ α →ₘ α) :
+lemma gfp_gfp (h : α →o α →o α) :
   gfp (gfp.comp h) = gfp h.on_diag :=
 @lfp_lfp (order_dual α) _ $ (order_hom.dual_iso (order_dual α)
   (order_dual α)).symm.to_order_embedding.to_order_hom.comp h.dual
 
 end eqn
 
 section prev_next
-variables [complete_lattice α] (f : α →ₘ α)
+variables [complete_lattice α] (f : α →o α)
 
 lemma gfp_const_inf_le (x : α) : gfp (const α x ⊓ f) ≤ x :=
 gfp_le _ $ λ b hb, hb.trans inf_le_left
@@ -209,7 +209,7 @@ namespace fixed_points
 
 open order_hom
 
-variables [complete_lattice α] (f : α →ₘ α)
+variables [complete_lattice α] (f : α →o α)
 
 instance : semilattice_sup (fixed_points f) :=
 { sup := λ x y, f.next_fixed (x ⊔ y) (f.le_map_sup_fixed_points x y),