mathlib3 documentation

algebra.order.group.order_iso

Inverse and multiplication as order isomorphisms in ordered groups #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

source
@[simp]
theorem order_iso.neg_apply (α : Type u) [add_group α] [has_le α] [covariant_class α α has_add.add has_le.le] [covariant_class α α (function.swap has_add.add) has_le.le] (ᾰ : α) :
⇑(order_iso.neg α) ᾰ = ⇑order_dual.to_dual (-ᾰ)
source
@[simp]
theorem order_iso.neg_symm_apply (α : Type u) [add_group α] [has_le α] [covariant_class α α has_add.add has_le.le] [covariant_class α α (function.swap has_add.add) has_le.le] (ᾰ : αᵒᵈ) :
⇑(rel_iso.symm (order_iso.neg α)) ᾰ = -⇑order_dual.of_dual ᾰ
source
def order_iso.inv (α : Type u) [group α] [has_le α] [covariant_class α α has_mul.mul has_le.le] [covariant_class α α (function.swap has_mul.mul) has_le.le] :
α ≃o αᵒᵈ

x ↦ x⁻¹ as an order-reversing equivalence.

Equations
source
@[simp]
theorem order_iso.inv_apply (α : Type u) [group α] [has_le α] [covariant_class α α has_mul.mul has_le.le] [covariant_class α α (function.swap has_mul.mul) has_le.le] (ᾰ : α) :
⇑(order_iso.inv α) ᾰ = ⇑order_dual.to_dual ᾰ⁻¹
source
def order_iso.neg (α : Type u) [add_group α] [has_le α] [covariant_class α α has_add.add has_le.le] [covariant_class α α (function.swap has_add.add) has_le.le] :
α ≃o αᵒᵈ

x ↦ -x as an order-reversing equivalence.

Equations
source
@[simp]
theorem order_iso.inv_symm_apply (α : Type u) [group α] [has_le α] [covariant_class α α has_mul.mul has_le.le] [covariant_class α α (function.swap has_mul.mul) has_le.le] (ᾰ : αᵒᵈ) :
⇑(rel_iso.symm (order_iso.inv α)) ᾰ = (⇑order_dual.of_dual ᾰ)⁻¹
source
theorem neg_le {α : Type u} [add_group α] [has_le α] [covariant_class α α has_add.add has_le.le] [covariant_class α α (function.swap has_add.add) has_le.le] {a b : α} :
-a ≤ b ↔ -b ≤ a
source
theorem inv_le' {α : Type u} [group α] [has_le α] [covariant_class α α has_mul.mul has_le.le] [covariant_class α α (function.swap has_mul.mul) has_le.le] {a b : α} :
a⁻¹ ≤ b ↔ b⁻¹ ≤ a
source
theorem inv_le_of_inv_le' {α : Type u} [group α] [has_le α] [covariant_class α α has_mul.mul has_le.le] [covariant_class α α (function.swap has_mul.mul) has_le.le] {a b : α} :
a⁻¹ ≤ b → b⁻¹ ≤ a

Alias of the forward direction of inv_le'.

source
theorem neg_le_of_neg_le {α : Type u} [add_group α] [has_le α] [covariant_class α α has_add.add has_le.le] [covariant_class α α (function.swap has_add.add) has_le.le] {a b : α} :
-a ≤ b → -b ≤ a

Alias of the forward direction of inv_le'.

source
theorem le_neg {α : Type u} [add_group α] [has_le α] [covariant_class α α has_add.add has_le.le] [covariant_class α α (function.swap has_add.add) has_le.le] {a b : α} :
a ≤ -b ↔ b ≤ -a
source
theorem le_inv' {α : Type u} [group α] [has_le α] [covariant_class α α has_mul.mul has_le.le] [covariant_class α α (function.swap has_mul.mul) has_le.le] {a b : α} :
a ≤ b⁻¹ ↔ b ≤ a⁻¹
source
@[simp]
theorem order_iso.sub_left_symm_apply {α : Type u} [add_group α] [has_le α] [covariant_class α α has_add.add has_le.le] [covariant_class α α (function.swap has_add.add) has_le.le] (a : α) (ᾰ : αᵒᵈ) :
⇑(rel_iso.symm (order_iso.sub_left a)) ᾰ = -⇑order_dual.of_dual ᾰ + a
source
@[simp]
theorem order_iso.div_left_symm_apply {α : Type u} [group α] [has_le α] [covariant_class α α has_mul.mul has_le.le] [covariant_class α α (function.swap has_mul.mul) has_le.le] (a : α) (ᾰ : αᵒᵈ) :
⇑(rel_iso.symm (order_iso.div_left a)) ᾰ = (⇑order_dual.of_dual ᾰ)⁻¹ * a
source
@[simp]
theorem order_iso.sub_left_apply {α : Type u} [add_group α] [has_le α] [covariant_class α α has_add.add has_le.le] [covariant_class α α (function.swap has_add.add) has_le.le] (a ᾰ : α) :
⇑(order_iso.sub_left a) ᾰ = ⇑order_dual.to_dual (a - ᾰ)
source
def order_iso.div_left {α : Type u} [group α] [has_le α] [covariant_class α α has_mul.mul has_le.le] [covariant_class α α (function.swap has_mul.mul) has_le.le] (a : α) :
α ≃o αᵒᵈ

x ↦ a / x as an order-reversing equivalence.

Equations
source
@[simp]
theorem order_iso.div_left_apply {α : Type u} [group α] [has_le α] [covariant_class α α has_mul.mul has_le.le] [covariant_class α α (function.swap has_mul.mul) has_le.le] (a ᾰ : α) :
⇑(order_iso.div_left a) ᾰ = ⇑order_dual.to_dual (a / ᾰ)
source
def order_iso.sub_left {α : Type u} [add_group α] [has_le α] [covariant_class α α has_add.add has_le.le] [covariant_class α α (function.swap has_add.add) has_le.le] (a : α) :
α ≃o αᵒᵈ

x ↦ a - x as an order-reversing equivalence.

Equations
source
theorem le_inv_of_le_inv {α : Type u} [group α] [has_le α] [covariant_class α α has_mul.mul has_le.le] [covariant_class α α (function.swap has_mul.mul) has_le.le] {a b : α} :
a ≤ b⁻¹ → b ≤ a⁻¹

Alias of the forward direction of le_inv'.

source
theorem le_neg_of_le_neg {α : Type u} [add_group α] [has_le α] [covariant_class α α has_add.add has_le.le] [covariant_class α α (function.swap has_add.add) has_le.le] {a b : α} :
a ≤ -b → b ≤ -a

Alias of the forward direction of le_inv'.

source
@[simp]
theorem order_iso.add_right_apply {α : Type u} [add_group α] [has_le α] [covariant_class α α (function.swap has_add.add) has_le.le] (a x : α) :
⇑(order_iso.add_right a) x = x + a
source
@[simp]
theorem order_iso.mul_right_apply {α : Type u} [group α] [has_le α] [covariant_class α α (function.swap has_mul.mul) has_le.le] (a x : α) :
⇑(order_iso.mul_right a) x = x * a
source
@[simp]
theorem order_iso.mul_right_to_equiv {α : Type u} [group α] [has_le α] [covariant_class α α (function.swap has_mul.mul) has_le.le] (a : α) :
(order_iso.mul_right a).to_equiv = equiv.mul_right a
source
def order_iso.add_right {α : Type u} [add_group α] [has_le α] [covariant_class α α (function.swap has_add.add) has_le.le] (a : α) :
α ≃o α

equiv.add_right as an order_iso. See also order_embedding.add_right.

Equations
source
def order_iso.mul_right {α : Type u} [group α] [has_le α] [covariant_class α α (function.swap has_mul.mul) has_le.le] (a : α) :
α ≃o α

equiv.mul_right as an order_iso. See also order_embedding.mul_right.

Equations
source
@[simp]
theorem order_iso.add_right_to_equiv {α : Type u} [add_group α] [has_le α] [covariant_class α α (function.swap has_add.add) has_le.le] (a : α) :
(order_iso.add_right a).to_equiv = equiv.add_right a
source
@[simp]
theorem order_iso.add_right_symm {α : Type u} [add_group α] [has_le α] [covariant_class α α (function.swap has_add.add) has_le.le] (a : α) :
(order_iso.add_right a).symm = order_iso.add_right (-a)
source
@[simp]
theorem order_iso.mul_right_symm {α : Type u} [group α] [has_le α] [covariant_class α α (function.swap has_mul.mul) has_le.le] (a : α) :
(order_iso.mul_right a).symm = order_iso.mul_right a⁻¹
source
@[simp]
theorem order_iso.div_right_symm_apply {α : Type u} [group α] [has_le α] [covariant_class α α (function.swap has_mul.mul) has_le.le] (a b : α) :
⇑(rel_iso.symm (order_iso.div_right a)) b = b * a
source
@[simp]
theorem order_iso.sub_right_symm_apply {α : Type u} [add_group α] [has_le α] [covariant_class α α (function.swap has_add.add) has_le.le] (a b : α) :
⇑(rel_iso.symm (order_iso.sub_right a)) b = b + a
source
def order_iso.div_right {α : Type u} [group α] [has_le α] [covariant_class α α (function.swap has_mul.mul) has_le.le] (a : α) :
α ≃o α

x ↦ x / a as an order isomorphism.

Equations
source
@[simp]
theorem order_iso.sub_right_apply {α : Type u} [add_group α] [has_le α] [covariant_class α α (function.swap has_add.add) has_le.le] (a b : α) :
⇑(order_iso.sub_right a) b = b - a
source
@[simp]
theorem order_iso.div_right_apply {α : Type u} [group α] [has_le α] [covariant_class α α (function.swap has_mul.mul) has_le.le] (a b : α) :
⇑(order_iso.div_right a) b = b / a
source
def order_iso.sub_right {α : Type u} [add_group α] [has_le α] [covariant_class α α (function.swap has_add.add) has_le.le] (a : α) :
α ≃o α

x ↦ x - a as an order isomorphism.

Equations
source
@[simp]
theorem order_iso.mul_left_to_equiv {α : Type u} [group α] [has_le α] [covariant_class α α has_mul.mul has_le.le] (a : α) :
(order_iso.mul_left a).to_equiv = equiv.mul_left a
source
@[simp]
theorem order_iso.add_left_to_equiv {α : Type u} [add_group α] [has_le α] [covariant_class α α has_add.add has_le.le] (a : α) :
(order_iso.add_left a).to_equiv = equiv.add_left a
source
@[simp]
theorem order_iso.add_left_apply {α : Type u} [add_group α] [has_le α] [covariant_class α α has_add.add has_le.le] (a x : α) :
⇑(order_iso.add_left a) x = a + x
source
def order_iso.add_left {α : Type u} [add_group α] [has_le α] [covariant_class α α has_add.add has_le.le] (a : α) :
α ≃o α

equiv.add_left as an order_iso. See also order_embedding.add_left.

Equations
source
@[simp]
theorem order_iso.mul_left_apply {α : Type u} [group α] [has_le α] [covariant_class α α has_mul.mul has_le.le] (a x : α) :
⇑(order_iso.mul_left a) x = a * x
source
def order_iso.mul_left {α : Type u} [group α] [has_le α] [covariant_class α α has_mul.mul has_le.le] (a : α) :
α ≃o α

equiv.mul_left as an order_iso. See also order_embedding.mul_left.

Equations
source
@[simp]
theorem order_iso.mul_left_symm {α : Type u} [group α] [has_le α] [covariant_class α α has_mul.mul has_le.le] (a : α) :
(order_iso.mul_left a).symm = order_iso.mul_left a⁻¹
source
@[simp]
theorem order_iso.add_left_symm {α : Type u} [add_group α] [has_le α] [covariant_class α α has_add.add has_le.le] (a : α) :
(order_iso.add_left a).symm = order_iso.add_left (-a)