# Ordered monoids #

This file develops some additional material on ordered monoids.

theorem Function.Injective.orderedAddCommMonoid.proof_1 {α : Type u_2} {β : Type u_1} [Add β] (f : βα) (hf : ) (mul : ∀ (x y : β), f (x + y) = f x + f y) (a : β) (b : β) (ab : a b) (c : β) :
f (c + a) f (c + b)
@[reducible]
def Function.Injective.orderedAddCommMonoid {α : Type u} {β : Type u_2} [Zero β] [Add β] [] (f : βα) (hf : ) (one : f 0 = 0) (mul : ∀ (x y : β), f (x + y) = f x + f y) (npow : ∀ (x : β) (n : ), f (n x) = n f x) :

Pullback an OrderedAddCommMonoid under an injective map.

Equations
Instances For
@[reducible]
def Function.Injective.orderedCommMonoid {α : Type u} {β : Type u_2} [One β] [Mul β] [Pow β ] (f : βα) (hf : ) (one : f 1 = 1) (mul : ∀ (x y : β), f (x * y) = f x * f y) (npow : ∀ (x : β) (n : ), f (x ^ n) = f x ^ n) :

Pullback an OrderedCommMonoid under an injective map. See note [reducible non-instances].

Equations
Instances For
@[reducible]
def Function.Injective.orderedCancelAddCommMonoid {α : Type u} {β : Type u_1} [Zero β] [Add β] [] (f : βα) (hf : ) (one : f 0 = 0) (mul : ∀ (x y : β), f (x + y) = f x + f y) (npow : ∀ (x : β) (n : ), f (n x) = n f x) :

Pullback an OrderedCancelAddCommMonoid under an injective map.

Equations
Instances For
theorem Function.Injective.orderedCancelAddCommMonoid.proof_1 {α : Type u_1} {β : Type u_2} [Add β] (f : βα) (mul : ∀ (x y : β), f (x + y) = f x + f y) (a : β) (b : β) (c : β) (bc : f (a + b) f (a + c)) :
f b f c
@[reducible]
def Function.Injective.orderedCancelCommMonoid {α : Type u} {β : Type u_1} [One β] [Mul β] [Pow β ] (f : βα) (hf : ) (one : f 1 = 1) (mul : ∀ (x y : β), f (x * y) = f x * f y) (npow : ∀ (x : β) (n : ), f (x ^ n) = f x ^ n) :

Pullback an OrderedCancelCommMonoid under an injective map. See note [reducible non-instances].

Equations
Instances For
@[reducible]
def Function.Injective.linearOrderedAddCommMonoid {α : Type u} {β : Type u_2} [Zero β] [Add β] [] [Sup β] [Inf β] (f : βα) (hf : ) (one : f 0 = 0) (mul : ∀ (x y : β), f (x + y) = f x + f y) (npow : ∀ (x : β) (n : ), f (n x) = n f x) (sup : ∀ (x y : β), f (x y) = max (f x) (f y)) (inf : ∀ (x y : β), f (x y) = min (f x) (f y)) :

Pullback an OrderedAddCommMonoid under an injective map.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[reducible]
def Function.Injective.linearOrderedCommMonoid {α : Type u} {β : Type u_2} [One β] [Mul β] [Pow β ] [Sup β] [Inf β] (f : βα) (hf : ) (one : f 1 = 1) (mul : ∀ (x y : β), f (x * y) = f x * f y) (npow : ∀ (x : β) (n : ), f (x ^ n) = f x ^ n) (sup : ∀ (x y : β), f (x y) = max (f x) (f y)) (inf : ∀ (x y : β), f (x y) = min (f x) (f y)) :

Pullback a LinearOrderedCommMonoid under an injective map. See note [reducible non-instances].

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[reducible]
def Function.Injective.linearOrderedCancelAddCommMonoid {α : Type u} {β : Type u_1} [Zero β] [Add β] [] [Sup β] [Inf β] (f : βα) (hf : ) (one : f 0 = 0) (mul : ∀ (x y : β), f (x + y) = f x + f y) (npow : ∀ (x : β) (n : ), f (n x) = n f x) (hsup : ∀ (x y : β), f (x y) = max (f x) (f y)) (hinf : ∀ (x y : β), f (x y) = min (f x) (f y)) :

Pullback a LinearOrderedCancelAddCommMonoid under an injective map.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[reducible]
def Function.Injective.linearOrderedCancelCommMonoid {α : Type u} {β : Type u_1} [One β] [Mul β] [Pow β ] [Sup β] [Inf β] (f : βα) (hf : ) (one : f 1 = 1) (mul : ∀ (x y : β), f (x * y) = f x * f y) (npow : ∀ (x : β) (n : ), f (x ^ n) = f x ^ n) (hsup : ∀ (x y : β), f (x y) = max (f x) (f y)) (hinf : ∀ (x y : β), f (x y) = min (f x) (f y)) :

Pullback a LinearOrderedCancelCommMonoid under an injective map. See note [reducible non-instances].

Equations
• One or more equations did not get rendered due to their size.
Instances For
theorem OrderEmbedding.addLeft.proof_1 {α : Type u_1} [Add α] [] [CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x < x_1] (m : α) :
∀ (x x_1 : α), x < x_1m + x < m + x_1
def OrderEmbedding.addLeft {α : Type u_2} [Add α] [] [CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x < x_1] (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
Instances For
@[simp]
theorem OrderEmbedding.mulLeft_apply {α : Type u_2} [Mul α] [] [CovariantClass α α (fun (x x_1 : α) => x * x_1) fun (x x_1 : α) => x < x_1] (m : α) (n : α) :
= m * n
@[simp]
theorem OrderEmbedding.addLeft_apply {α : Type u_2} [Add α] [] [CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x < x_1] (m : α) (n : α) :
= m + n
def OrderEmbedding.mulLeft {α : Type u_2} [Mul α] [] [CovariantClass α α (fun (x x_1 : α) => x * x_1) fun (x x_1 : α) => x < x_1] (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
Instances For
def OrderEmbedding.addRight {α : Type u_2} [Add α] [] [CovariantClass α α (Function.swap fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x < x_1] (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
Instances For
theorem OrderEmbedding.addRight.proof_1 {α : Type u_1} [Add α] [] [CovariantClass α α (Function.swap fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x < x_1] (m : α) :
∀ (x x_1 : α), x < x_1x + m < x_1 + m
@[simp]
theorem OrderEmbedding.addRight_apply {α : Type u_2} [Add α] [] [CovariantClass α α (Function.swap fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x < x_1] (m : α) (n : α) :
= n + m
@[simp]
theorem OrderEmbedding.mulRight_apply {α : Type u_2} [Mul α] [] [CovariantClass α α (Function.swap fun (x x_1 : α) => x * x_1) fun (x x_1 : α) => x < x_1] (m : α) (n : α) :
= n * m
def OrderEmbedding.mulRight {α : Type u_2} [Mul α] [] [CovariantClass α α (Function.swap fun (x x_1 : α) => x * x_1) fun (x x_1 : α) => x < x_1] (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
Instances For