Ordered monoids #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
This file develops some additional material on ordered monoids.
@[reducible]
def
function.injective.ordered_comm_monoid
{α : Type u}
[ordered_comm_monoid α]
{β : Type u_1}
[has_one β]
[has_mul β]
[has_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) :
Pullback an ordered_comm_monoid under an injective map.
See note [reducible non-instances].
Equations
- function.injective.ordered_comm_monoid f hf one mul npow = {mul := comm_monoid.mul (function.injective.comm_monoid f hf one mul npow), mul_assoc := _, one := comm_monoid.one (function.injective.comm_monoid f hf one mul npow), one_mul := _, mul_one := _, npow := comm_monoid.npow (function.injective.comm_monoid f hf one mul npow), npow_zero' := _, npow_succ' := _, mul_comm := _, le := partial_order.le (partial_order.lift f hf), lt := partial_order.lt (partial_order.lift f hf), le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, mul_le_mul_left := _}
@[reducible]
def
function.injective.ordered_add_comm_monoid
{α : Type u}
[ordered_add_comm_monoid α]
{β : Type u_1}
[has_zero β]
[has_add β]
[has_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) :
Pullback an ordered_add_comm_monoid under an injective map.
Equations
- function.injective.ordered_add_comm_monoid f hf one mul npow = {add := add_comm_monoid.add (function.injective.add_comm_monoid f hf one mul npow), add_assoc := _, zero := add_comm_monoid.zero (function.injective.add_comm_monoid f hf one mul npow), zero_add := _, add_zero := _, nsmul := add_comm_monoid.nsmul (function.injective.add_comm_monoid f hf one mul npow), nsmul_zero' := _, nsmul_succ' := _, add_comm := _, le := partial_order.le (partial_order.lift f hf), lt := partial_order.lt (partial_order.lift f hf), le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, add_le_add_left := _}
@[reducible]
def
function.injective.linear_ordered_comm_monoid
{α : Type u}
[linear_ordered_comm_monoid α]
{β : Type u_1}
[has_one β]
[has_mul β]
[has_pow β ℕ]
[has_sup β]
[has_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) = linear_order.max (f x) (f y))
(hinf : ∀ (x y : β), f (x ⊓ y) = linear_order.min (f x) (f y)) :
Pullback a linear_ordered_comm_monoid under an injective map.
See note [reducible non-instances].
Equations
- function.injective.linear_ordered_comm_monoid f hf one mul npow hsup hinf = {le := ordered_comm_monoid.le (function.injective.ordered_comm_monoid f hf one mul npow), lt := ordered_comm_monoid.lt (function.injective.ordered_comm_monoid f hf one mul npow), le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_total := _, decidable_le := linear_order.decidable_le (linear_order.lift f hf hsup hinf), decidable_eq := linear_order.decidable_eq (linear_order.lift f hf hsup hinf), decidable_lt := linear_order.decidable_lt (linear_order.lift f hf hsup hinf), max := linear_order.max (linear_order.lift f hf hsup hinf), max_def := _, min := linear_order.min (linear_order.lift f hf hsup hinf), min_def := _, mul := ordered_comm_monoid.mul (function.injective.ordered_comm_monoid f hf one mul npow), mul_assoc := _, one := ordered_comm_monoid.one (function.injective.ordered_comm_monoid f hf one mul npow), one_mul := _, mul_one := _, npow := ordered_comm_monoid.npow (function.injective.ordered_comm_monoid f hf one mul npow), npow_zero' := _, npow_succ' := _, mul_comm := _, mul_le_mul_left := _}
@[reducible]
def
function.injective.linear_ordered_add_comm_monoid
{α : Type u}
[linear_ordered_add_comm_monoid α]
{β : Type u_1}
[has_zero β]
[has_add β]
[has_smul ℕ β]
[has_sup β]
[has_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) = linear_order.max (f x) (f y))
(hinf : ∀ (x y : β), f (x ⊓ y) = linear_order.min (f x) (f y)) :
Pullback an ordered_add_comm_monoid under an injective map.
Equations
- function.injective.linear_ordered_add_comm_monoid f hf one mul npow hsup hinf = {le := ordered_add_comm_monoid.le (function.injective.ordered_add_comm_monoid f hf one mul npow), lt := ordered_add_comm_monoid.lt (function.injective.ordered_add_comm_monoid f hf one mul npow), le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_total := _, decidable_le := linear_order.decidable_le (linear_order.lift f hf hsup hinf), decidable_eq := linear_order.decidable_eq (linear_order.lift f hf hsup hinf), decidable_lt := linear_order.decidable_lt (linear_order.lift f hf hsup hinf), max := linear_order.max (linear_order.lift f hf hsup hinf), max_def := _, min := linear_order.min (linear_order.lift f hf hsup hinf), min_def := _, add := ordered_add_comm_monoid.add (function.injective.ordered_add_comm_monoid f hf one mul npow), add_assoc := _, zero := ordered_add_comm_monoid.zero (function.injective.ordered_add_comm_monoid f hf one mul npow), zero_add := _, add_zero := _, nsmul := ordered_add_comm_monoid.nsmul (function.injective.ordered_add_comm_monoid f hf one mul npow), nsmul_zero' := _, nsmul_succ' := _, add_comm := _, add_le_add_left := _}
@[simp]
theorem
order_embedding.add_left_apply
{α : Type u_1}
[has_add α]
[linear_order α]
[covariant_class α α has_add.add has_lt.lt]
(m n : α) :
⇑(order_embedding.add_left m) n = m + n
def
order_embedding.mul_left
{α : Type u_1}
[has_mul α]
[linear_order α]
[covariant_class α α has_mul.mul has_lt.lt]
(m : α) :
α ↪o α
The order embedding sending b to a * b, for some fixed a.
See also order_iso.mul_left when working in an ordered group.
Equations
- order_embedding.mul_left m = order_embedding.of_strict_mono (λ (n : α), m * n) _
def
order_embedding.add_left
{α : Type u_1}
[has_add α]
[linear_order α]
[covariant_class α α has_add.add has_lt.lt]
(m : α) :
α ↪o α
The order embedding sending b to a + b, for some fixed a.
See also order_iso.add_left when working in an additive ordered group.
Equations
- order_embedding.add_left m = order_embedding.of_strict_mono (λ (n : α), m + n) _
@[simp]
theorem
order_embedding.mul_left_apply
{α : Type u_1}
[has_mul α]
[linear_order α]
[covariant_class α α has_mul.mul has_lt.lt]
(m n : α) :
⇑(order_embedding.mul_left m) n = m * n
@[simp]
theorem
order_embedding.mul_right_apply
{α : Type u_1}
[has_mul α]
[linear_order α]
[covariant_class α α (function.swap has_mul.mul) has_lt.lt]
(m n : α) :
⇑(order_embedding.mul_right m) n = n * m
def
order_embedding.mul_right
{α : Type u_1}
[has_mul α]
[linear_order α]
[covariant_class α α (function.swap has_mul.mul) has_lt.lt]
(m : α) :
α ↪o α
The order embedding sending b to b * a, for some fixed a.
See also order_iso.mul_right when working in an ordered group.
Equations
- order_embedding.mul_right m = order_embedding.of_strict_mono (λ (n : α), n * m) _
@[simp]
theorem
order_embedding.add_right_apply
{α : Type u_1}
[has_add α]
[linear_order α]
[covariant_class α α (function.swap has_add.add) has_lt.lt]
(m n : α) :
⇑(order_embedding.add_right m) n = n + m
def
order_embedding.add_right
{α : Type u_1}
[has_add α]
[linear_order α]
[covariant_class α α (function.swap has_add.add) has_lt.lt]
(m : α) :
α ↪o α
The order embedding sending b to b + a, for some fixed a.
See also order_iso.add_right when working in an additive ordered group.
Equations
- order_embedding.add_right m = order_embedding.of_strict_mono (λ (n : α), n + m) _