Ordered monoids

This file develops some additional material on ordered monoids.

theorem Function.Injective.isOrderedMonoid {α : Type u} {β : Type u_1} [CommMonoid α] [PartialOrder α] [IsOrderedMonoid α] [CommMonoid β] [PartialOrder β] (f : β → α) (mul : ∀ (x y : β), f (x * y) = f x * f y) (le : ∀ {x y : β}, f x ≤ f y ↔ x ≤ y) : IsOrderedMonoid β

Pullback an IsOrderedMonoid under an injective map.

theorem Function.Injective.isOrderedAddMonoid {α : Type u} {β : Type u_1} [AddCommMonoid α] [PartialOrder α] [IsOrderedAddMonoid α] [AddCommMonoid β] [PartialOrder β] (f : β → α) (add : ∀ (x y : β), f (x + y) = f x + f y) (le : ∀ {x y : β}, f x ≤ f y ↔ x ≤ y) : IsOrderedAddMonoid β

Pullback an IsOrderedAddMonoid under an injective map.

theorem StrictMono.isOrderedMonoid {α : Type u} {β : Type u_1} [CommMonoid α] [PartialOrder α] [IsOrderedMonoid α] [CommMonoid β] [LinearOrder β] (f : β → α) (hf : StrictMono f) (mul : ∀ (x y : β), f (x * y) = f x * f y) : IsOrderedMonoid β

Pullback an IsOrderedMonoid under a strictly monotone map.

theorem StrictMono.isOrderedAddMonoid {α : Type u} {β : Type u_1} [AddCommMonoid α] [PartialOrder α] [IsOrderedAddMonoid α] [AddCommMonoid β] [LinearOrder β] (f : β → α) (hf : StrictMono f) (add : ∀ (x y : β), f (x + y) = f x + f y) : IsOrderedAddMonoid β

Pullback an IsOrderedAddMonoid under a strictly monotone map.

theorem Function.Injective.isOrderedCancelMonoid {α : Type u} {β : Type u_1} [CommMonoid α] [PartialOrder α] [IsOrderedCancelMonoid α] [CommMonoid β] [PartialOrder β] (f : β → α) (mul : ∀ (x y : β), f (x * y) = f x * f y) (le : ∀ {x y : β}, f x ≤ f y ↔ x ≤ y) : IsOrderedCancelMonoid β

Pullback an IsOrderedCancelMonoid under an injective map.

theorem Function.Injective.isOrderedCancelAddMonoid {α : Type u} {β : Type u_1} [AddCommMonoid α] [PartialOrder α] [IsOrderedCancelAddMonoid α] [AddCommMonoid β] [PartialOrder β] (f : β → α) (add : ∀ (x y : β), f (x + y) = f x + f y) (le : ∀ {x y : β}, f x ≤ f y ↔ x ≤ y) : IsOrderedCancelAddMonoid β

Pullback an IsOrderedCancelAddMonoid under an injective map.

theorem StrictMono.isOrderedCancelMonoid {α : Type u} {β : Type u_1} [CommMonoid α] [PartialOrder α] [IsOrderedCancelMonoid α] [CommMonoid β] [LinearOrder β] (f : β → α) (hf : StrictMono f) (mul : ∀ (x y : β), f (x * y) = f x * f y) : IsOrderedCancelMonoid β

Pullback an IsOrderedCancelMonoid under a strictly monotone map.

theorem StrictMono.isOrderedAddCancelMonoid {α : Type u} {β : Type u_1} [AddCommMonoid α] [PartialOrder α] [IsOrderedCancelAddMonoid α] [AddCommMonoid β] [LinearOrder β] (f : β → α) (hf : StrictMono f) (add : ∀ (x y : β), f (x + y) = f x + f y) : IsOrderedCancelAddMonoid β

Pullback an IsOrderedAddCancelMonoid under a strictly monotone map.

@[deprecated Function.Injective.isOrderedMonoid (since := "2025-04-10")]

theorem Function.Injective.orderedCommMonoid {α : Type u} {β : Type u_1} [CommMonoid α] [PartialOrder α] [IsOrderedMonoid α] [CommMonoid β] [PartialOrder β] (f : β → α) (mul : ∀ (x y : β), f (x * y) = f x * f y) (le : ∀ {x y : β}, f x ≤ f y ↔ x ≤ y) : IsOrderedMonoid β

Alias of Function.Injective.isOrderedMonoid.

---

Pullback an IsOrderedMonoid under an injective map.

@[deprecated Function.Injective.isOrderedAddMonoid (since := "2025-04-10")]

theorem Function.Injective.orderedAddCommMonoid {α : Type u} {β : Type u_1} [AddCommMonoid α] [PartialOrder α] [IsOrderedAddMonoid α] [AddCommMonoid β] [PartialOrder β] (f : β → α) (add : ∀ (x y : β), f (x + y) = f x + f y) (le : ∀ {x y : β}, f x ≤ f y ↔ x ≤ y) : IsOrderedAddMonoid β

Alias of Function.Injective.isOrderedAddMonoid.

---

Pullback an IsOrderedAddMonoid under an injective map.

@[deprecated Function.Injective.isOrderedCancelMonoid (since := "2025-04-10")]

theorem Function.Injective.orderedCancelCommMonoid {α : Type u} {β : Type u_1} [CommMonoid α] [PartialOrder α] [IsOrderedCancelMonoid α] [CommMonoid β] [PartialOrder β] (f : β → α) (mul : ∀ (x y : β), f (x * y) = f x * f y) (le : ∀ {x y : β}, f x ≤ f y ↔ x ≤ y) : IsOrderedCancelMonoid β

Alias of Function.Injective.isOrderedCancelMonoid.

---

Pullback an IsOrderedCancelMonoid under an injective map.

@[deprecated Function.Injective.isOrderedCancelAddMonoid (since := "2025-04-10")]

theorem Function.Injective.orderedCancelAddCommMonoid {α : Type u} {β : Type u_1} [AddCommMonoid α] [PartialOrder α] [IsOrderedCancelAddMonoid α] [AddCommMonoid β] [PartialOrder β] (f : β → α) (add : ∀ (x y : β), f (x + y) = f x + f y) (le : ∀ {x y : β}, f x ≤ f y ↔ x ≤ y) : IsOrderedCancelAddMonoid β

Alias of Function.Injective.isOrderedCancelAddMonoid.

---

Pullback an IsOrderedCancelAddMonoid under an injective map.

@[deprecated Function.Injective.isOrderedMonoid (since := "2025-04-10")]

theorem Function.Injective.linearOrderedCommMonoid {α : Type u} {β : Type u_1} [CommMonoid α] [PartialOrder α] [IsOrderedMonoid α] [CommMonoid β] [PartialOrder β] (f : β → α) (mul : ∀ (x y : β), f (x * y) = f x * f y) (le : ∀ {x y : β}, f x ≤ f y ↔ x ≤ y) : IsOrderedMonoid β

Alias of Function.Injective.isOrderedMonoid.

---

Pullback an IsOrderedMonoid under an injective map.

@[deprecated Function.Injective.isOrderedAddMonoid (since := "2025-04-10")]

theorem Function.Injective.linearOrderedAddCommMonoid {α : Type u} {β : Type u_1} [AddCommMonoid α] [PartialOrder α] [IsOrderedAddMonoid α] [AddCommMonoid β] [PartialOrder β] (f : β → α) (add : ∀ (x y : β), f (x + y) = f x + f y) (le : ∀ {x y : β}, f x ≤ f y ↔ x ≤ y) : IsOrderedAddMonoid β

Alias of Function.Injective.isOrderedAddMonoid.

---

Pullback an IsOrderedAddMonoid under an injective map.

@[deprecated Function.Injective.isOrderedCancelMonoid (since := "2025-04-10")]

theorem Function.Injective.linearOrderedCancelCommMonoid {α : Type u} {β : Type u_1} [CommMonoid α] [PartialOrder α] [IsOrderedCancelMonoid α] [CommMonoid β] [PartialOrder β] (f : β → α) (mul : ∀ (x y : β), f (x * y) = f x * f y) (le : ∀ {x y : β}, f x ≤ f y ↔ x ≤ y) : IsOrderedCancelMonoid β

Alias of Function.Injective.isOrderedCancelMonoid.

---

Pullback an IsOrderedCancelMonoid under an injective map.

@[deprecated Function.Injective.isOrderedCancelAddMonoid (since := "2025-04-10")]

theorem Function.Injective.linearOrderedCancelAddCommMonoid {α : Type u} {β : Type u_1} [AddCommMonoid α] [PartialOrder α] [IsOrderedCancelAddMonoid α] [AddCommMonoid β] [PartialOrder β] (f : β → α) (add : ∀ (x y : β), f (x + y) = f x + f y) (le : ∀ {x y : β}, f x ≤ f y ↔ x ≤ y) : IsOrderedCancelAddMonoid β

Alias of Function.Injective.isOrderedCancelAddMonoid.

---

Pullback an IsOrderedCancelAddMonoid under an injective map.

@[deprecated Function.Injective.isOrderedMonoid (since := "2025-04-10")]

theorem Function.Injective.orderedCommGroup {α : Type u} {β : Type u_1} [CommMonoid α] [PartialOrder α] [IsOrderedMonoid α] [CommMonoid β] [PartialOrder β] (f : β → α) (mul : ∀ (x y : β), f (x * y) = f x * f y) (le : ∀ {x y : β}, f x ≤ f y ↔ x ≤ y) : IsOrderedMonoid β

Alias of Function.Injective.isOrderedMonoid.

---

Pullback an IsOrderedMonoid under an injective map.

@[deprecated Function.Injective.isOrderedAddMonoid (since := "2025-04-10")]

theorem Function.Injective.orderedAddCommGroup {α : Type u} {β : Type u_1} [AddCommMonoid α] [PartialOrder α] [IsOrderedAddMonoid α] [AddCommMonoid β] [PartialOrder β] (f : β → α) (add : ∀ (x y : β), f (x + y) = f x + f y) (le : ∀ {x y : β}, f x ≤ f y ↔ x ≤ y) : IsOrderedAddMonoid β

Alias of Function.Injective.isOrderedAddMonoid.

---

Pullback an IsOrderedAddMonoid under an injective map.

@[deprecated Function.Injective.isOrderedMonoid (since := "2025-04-10")]

theorem Function.Injective.linearOrderedCommGroup {α : Type u} {β : Type u_1} [CommMonoid α] [PartialOrder α] [IsOrderedMonoid α] [CommMonoid β] [PartialOrder β] (f : β → α) (mul : ∀ (x y : β), f (x * y) = f x * f y) (le : ∀ {x y : β}, f x ≤ f y ↔ x ≤ y) : IsOrderedMonoid β

Alias of Function.Injective.isOrderedMonoid.

---

Pullback an IsOrderedMonoid under an injective map.

@[deprecated Function.Injective.isOrderedAddMonoid (since := "2025-04-10")]

theorem Function.Injective.linearOrderedAddCommGroup {α : Type u} {β : Type u_1} [AddCommMonoid α] [PartialOrder α] [IsOrderedAddMonoid α] [AddCommMonoid β] [PartialOrder β] (f : β → α) (add : ∀ (x y : β), f (x + y) = f x + f y) (le : ∀ {x y : β}, f x ≤ f y ↔ x ≤ y) : IsOrderedAddMonoid β

Alias of Function.Injective.isOrderedAddMonoid.

---

Pullback an IsOrderedAddMonoid under an injective map.

def OrderEmbedding.mulLeft {α : Type u_2} [Mul α] [LinearOrder α] [MulLeftStrictMono α] (m : α) : α ↪o α

The order embedding sending b to a * b, for some fixed a. See also OrderIso.mulLeft when working in an ordered group.

Equations

• OrderEmbedding.mulLeft m = OrderEmbedding.ofStrictMono (fun (n : α) => m * n) ⋯

def OrderEmbedding.addLeft {α : Type u_2} [Add α] [LinearOrder α] [AddLeftStrictMono α] (m : α) : α ↪o α

The order embedding sending b to a + b, for some fixed a. See also OrderIso.addLeft when working in an additive ordered group.

Equations

• OrderEmbedding.addLeft m = OrderEmbedding.ofStrictMono (fun (n : α) => m + n) ⋯

@[simp]

theorem OrderEmbedding.addLeft_apply {α : Type u_2} [Add α] [LinearOrder α] [AddLeftStrictMono α] (m n : α) : (addLeft m) n = m + n

@[simp]

theorem OrderEmbedding.mulLeft_apply {α : Type u_2} [Mul α] [LinearOrder α] [MulLeftStrictMono α] (m n : α) : (mulLeft m) n = m * n

def OrderEmbedding.mulRight {α : Type u_2} [Mul α] [LinearOrder α] [MulRightStrictMono α] (m : α) : α ↪o α

The order embedding sending b to b * a, for some fixed a. See also OrderIso.mulRight when working in an ordered group.

Equations

• OrderEmbedding.mulRight m = OrderEmbedding.ofStrictMono (fun (n : α) => n * m) ⋯

def OrderEmbedding.addRight {α : Type u_2} [Add α] [LinearOrder α] [AddRightStrictMono α] (m : α) : α ↪o α

The order embedding sending b to b + a, for some fixed a. See also OrderIso.addRight when working in an additive ordered group.

Equations

• OrderEmbedding.addRight m = OrderEmbedding.ofStrictMono (fun (n : α) => n + m) ⋯

@[simp]

theorem OrderEmbedding.addRight_apply {α : Type u_2} [Add α] [LinearOrder α] [AddRightStrictMono α] (m n : α) : (addRight m) n = n + m

@[simp]

theorem OrderEmbedding.mulRight_apply {α : Type u_2} [Mul α] [LinearOrder α] [MulRightStrictMono α] (m n : α) : (mulRight m) n = n * m