Ordered monoids

This file develops some additional material on ordered monoids.

theorem Function.Injective.orderedAddCommMonoid.proof_1 {α : Type u_2} [OrderedAddCommMonoid α] {β : Type u_1} [Add β] (f : β → α) (hf : Function.Injective f) (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} [OrderedAddCommMonoid α] {β : Type u_2} [Zero β] [Add β] [SMul ℕ β] (f : β → α) (hf : Function.Injective f) (one : f 0 = 0) (mul : ∀ (x y : β), f (x + y) = f x + f y) (npow : ∀ (x : β) (n : ℕ), f (n • x) = n • f x) : OrderedAddCommMonoid β

Pullback an OrderedAddCommMonoid under an injective map.

Equations

• Function.Injective.orderedAddCommMonoid f hf one mul npow = OrderedAddCommMonoid.mk ⋯

@[reducible]

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

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

Equations

• Function.Injective.orderedCommMonoid f hf one mul npow = OrderedCommMonoid.mk ⋯

@[reducible]

def Function.Injective.orderedCancelAddCommMonoid {α : Type u} {β : Type u_1} [OrderedCancelAddCommMonoid α] [Zero β] [Add β] [SMul ℕ β] (f : β → α) (hf : Function.Injective f) (one : f 0 = 0) (mul : ∀ (x y : β), f (x + y) = f x + f y) (npow : ∀ (x : β) (n : ℕ), f (n • x) = n • f x) : OrderedCancelAddCommMonoid β

Pullback an OrderedCancelAddCommMonoid under an injective map.

Equations

• Function.Injective.orderedCancelAddCommMonoid f hf one mul npow = OrderedCancelAddCommMonoid.mk ⋯

theorem Function.Injective.orderedCancelAddCommMonoid.proof_1 {α : Type u_1} {β : Type u_2} [OrderedCancelAddCommMonoid α] [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} [OrderedCancelCommMonoid α] [One β] [Mul β] [Pow β ℕ] (f : β → α) (hf : Function.Injective f) (one : f 1 = 1) (mul : ∀ (x y : β), f (x * y) = f x * f y) (npow : ∀ (x : β) (n : ℕ), f (x ^ n) = f x ^ n) : OrderedCancelCommMonoid β

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

Equations

• Function.Injective.orderedCancelCommMonoid f hf one mul npow = OrderedCancelCommMonoid.mk ⋯

@[reducible]

def Function.Injective.linearOrderedAddCommMonoid {α : Type u} [LinearOrderedAddCommMonoid α] {β : Type u_2} [Zero β] [Add β] [SMul ℕ β] [Sup β] [Inf β] (f : β → α) (hf : Function.Injective f) (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)) : LinearOrderedAddCommMonoid β

Pullback an OrderedAddCommMonoid under an injective map.

Equations

• One or more equations did not get rendered due to their size.

@[reducible]

def Function.Injective.linearOrderedCommMonoid {α : Type u} [LinearOrderedCommMonoid α] {β : Type u_2} [One β] [Mul β] [Pow β ℕ] [Sup β] [Inf β] (f : β → α) (hf : Function.Injective f) (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)) : LinearOrderedCommMonoid β

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.

@[reducible]

def Function.Injective.linearOrderedCancelAddCommMonoid {α : Type u} {β : Type u_1} [LinearOrderedCancelAddCommMonoid α] [Zero β] [Add β] [SMul ℕ β] [Sup β] [Inf β] (f : β → α) (hf : Function.Injective f) (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)) : LinearOrderedCancelAddCommMonoid β

Pullback a LinearOrderedCancelAddCommMonoid under an injective map.

Equations

• One or more equations did not get rendered due to their size.

@[reducible]

def Function.Injective.linearOrderedCancelCommMonoid {α : Type u} {β : Type u_1} [LinearOrderedCancelCommMonoid α] [One β] [Mul β] [Pow β ℕ] [Sup β] [Inf β] (f : β → α) (hf : Function.Injective f) (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)) : LinearOrderedCancelCommMonoid β

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.

theorem OrderEmbedding.addLeft.proof_1 {α : Type u_1} [Add α] [LinearOrder α] [CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x < x_1] (m : α) : ∀ (x x_1 : α), x < x_1 → m + x < m + x_1

def OrderEmbedding.addLeft {α : Type u_2} [Add α] [LinearOrder α] [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

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

@[simp]

theorem OrderEmbedding.mulLeft_apply {α : Type u_2} [Mul α] [LinearOrder α] [CovariantClass α α (fun (x x_1 : α) => x * x_1) fun (x x_1 : α) => x < x_1] (m : α) (n : α) : (OrderEmbedding.mulLeft m) n = m * n

@[simp]

theorem OrderEmbedding.addLeft_apply {α : Type u_2} [Add α] [LinearOrder α] [CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x < x_1] (m : α) (n : α) : (OrderEmbedding.addLeft m) n = m + n

def OrderEmbedding.mulLeft {α : Type u_2} [Mul α] [LinearOrder α] [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

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

def OrderEmbedding.addRight {α : Type u_2} [Add α] [LinearOrder α] [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

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

theorem OrderEmbedding.addRight.proof_1 {α : Type u_1} [Add α] [LinearOrder α] [CovariantClass α α (Function.swap fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x < x_1] (m : α) : ∀ (x x_1 : α), x < x_1 → x + m < x_1 + m

@[simp]

theorem OrderEmbedding.addRight_apply {α : Type u_2} [Add α] [LinearOrder α] [CovariantClass α α (Function.swap fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x < x_1] (m : α) (n : α) : (OrderEmbedding.addRight m) n = n + m

@[simp]

theorem OrderEmbedding.mulRight_apply {α : Type u_2} [Mul α] [LinearOrder α] [CovariantClass α α (Function.swap fun (x x_1 : α) => x * x_1) fun (x x_1 : α) => x < x_1] (m : α) (n : α) : (OrderEmbedding.mulRight m) n = n * m

def OrderEmbedding.mulRight {α : Type u_2} [Mul α] [LinearOrder α] [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

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