Basic results on ordered cancellative monoids.

We pull back ordered cancellative monoids along injective maps.

theorem Function.Injective.orderedCancelAddCommMonoid.proof_1 {α : Type u_1} [OrderedCancelAddCommMonoid α] {β : 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.orderedCancelAddCommMonoid {α : Type u} [OrderedCancelAddCommMonoid α] {β : Type u_1} [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

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

@[reducible]

def Function.Injective.orderedCancelCommMonoid {α : Type u} [OrderedCancelCommMonoid α] {β : Type u_1} [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

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

theorem Function.Injective.linearOrderedCancelAddCommMonoid.proof_1 {α : Type u_2} [LinearOrderedCancelAddCommMonoid α] {β : Type u_1} [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)) (a : β) (b : β) : a ≤ b ∨ b ≤ a

theorem Function.Injective.linearOrderedCancelAddCommMonoid.proof_4 {α : Type u_2} [LinearOrderedCancelAddCommMonoid α] {β : Type u_1} [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)) (a : β) (b : β) : compare a b = compareOfLessAndEq a b

@[reducible]

def Function.Injective.linearOrderedCancelAddCommMonoid {α : Type u} [LinearOrderedCancelAddCommMonoid α] {β : Type u_1} [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.

theorem Function.Injective.linearOrderedCancelAddCommMonoid.proof_3 {α : Type u_2} [LinearOrderedCancelAddCommMonoid α] {β : Type u_1} [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)) (a : β) (b : β) : max a b = if a ≤ b then b else a

theorem Function.Injective.linearOrderedCancelAddCommMonoid.proof_2 {α : Type u_2} [LinearOrderedCancelAddCommMonoid α] {β : Type u_1} [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)) (a : β) (b : β) : min a b = if a ≤ b then a else b

@[reducible]

def Function.Injective.linearOrderedCancelCommMonoid {α : Type u} [LinearOrderedCancelCommMonoid α] {β : Type u_1} [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.