Ordered monoids

This file develops some additional material on ordered monoids.

ink

def Function.Injective.orderedAddCommMonoid.proof_1 {α : Type u_2} [inst : OrderedAddCommMonoid α] {β : Type u_1} [inst : 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)

Equations

• (_ : f (c + a) ≤ f (c + b)) = (_ : f (c + a) ≤ f (c + b))

ink

def Function.Injective.orderedAddCommMonoid {α : Type u} [inst : OrderedAddCommMonoid α] {β : Type u_1} [inst : Zero β] [inst : Add β] [inst : 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

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

ink

def Function.Injective.orderedCommMonoid {α : Type u} [inst : OrderedCommMonoid α] {β : Type u_1} [inst : One β] [inst : Mul β] [inst : 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

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

ink

def Function.Injective.linearOrderedAddCommMonoid {α : Type u} [inst : LinearOrderedAddCommMonoid α] {β : Type u_1} [inst : Zero β] [inst : Add β] [inst : SMul ℕ β] [inst : Sup β] [inst : 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)) : LinearOrderedAddCommMonoid β

Pullback an OrderedAddCommMonoid under an injective map.

Equations

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

ink

def Function.Injective.linearOrderedCommMonoid {α : Type u} [inst : LinearOrderedCommMonoid α] {β : Type u_1} [inst : One β] [inst : Mul β] [inst : Pow β ℕ] [inst : Sup β] [inst : 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)) : 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.

ink

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

Equations

• (_ : m + x < m + x) = (_ : m + x < m + x)

ink

def OrderEmbedding.addLeft {α : Type u_1} [inst : Add α] [inst : LinearOrder α] [inst : 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) (_ : ∀ (x x_1 : α), x < x_1 → m + x < m + x_1)

ink

@[simp]

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

ink

@[simp]

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

ink

def OrderEmbedding.mulLeft {α : Type u_1} [inst : Mul α] [inst : LinearOrder α] [inst : 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) (_ : ∀ (x x_1 : α), x < x_1 → m * x < m * x_1)

ink

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

Equations

• (_ : x + m < x + m) = (_ : x + m < x + m)

ink

def OrderEmbedding.addRight {α : Type u_1} [inst : Add α] [inst : LinearOrder α] [inst : 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) (_ : ∀ (x x_1 : α), x < x_1 → x + m < x_1 + m)

ink

@[simp]

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

ink

@[simp]

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

ink

def OrderEmbedding.mulRight {α : Type u_1} [inst : Mul α] [inst : LinearOrder α] [inst : 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) (_ : ∀ (x x_1 : α), x < x_1 → x * m < x_1 * m)