Mathlib.Algebra.Order.Group.OrderIso

OrderIso.inv definition

: α ≃o αᵒᵈ

Full source

/-- `x ↦ x⁻¹` as an order-reversing equivalence. -/
@[to_additive (attr := simps!) "`x ↦ -x` as an order-reversing equivalence."]
def OrderIso.inv : α ≃o αᵒᵈ where
  toEquiv := (Equiv.inv α).trans OrderDual.toDual
  map_rel_iff' {_ _} := inv_le_inv_iff (α := α)

Inversion as an order-reversing isomorphism

Informal description

The inversion operation $x \mapsto x^{-1}$ defines an order-reversing isomorphism between a group $\alpha$ and its order dual $\alpha^{\text{op}}$. Specifically, for any elements $a, b \in \alpha$, we have $a^{-1} \leq b^{-1}$ in $\alpha$ if and only if $b \leq a$ in $\alpha^{\text{op}}$.

inv_le' theorem

: a⁻¹ ≤ b ↔ b⁻¹ ≤ a

Full source

@[to_additive neg_le]
theorem inv_le' : a⁻¹a⁻¹ ≤ b ↔ b⁻¹ ≤ a :=
  (OrderIso.inv α).symm_apply_le

Inverse Inequality in Ordered Groups: $a^{-1} \leq b \leftrightarrow b^{-1} \leq a$

Informal description

For any elements $a$ and $b$ in an ordered group, the inequality $a^{-1} \leq b$ holds if and only if $b^{-1} \leq a$.

le_inv' theorem

: a ≤ b⁻¹ ↔ b ≤ a⁻¹

Full source

@[to_additive le_neg]
theorem le_inv' : a ≤ b⁻¹ ↔ b ≤ a⁻¹ :=
  (OrderIso.inv α).le_symm_apply

Order-Reversing Property of Inversion: $a \leq b^{-1} \leftrightarrow b \leq a^{-1}$

Informal description

For any elements $a$ and $b$ in an ordered group, $a \leq b^{-1}$ if and only if $b \leq a^{-1}$.

OrderIso.divLeft definition

(a : α) : α ≃o αᵒᵈ

Full source

/-- `x ↦ a / x` as an order-reversing equivalence. -/
@[to_additive (attr := simps!) "`x ↦ a - x` as an order-reversing equivalence."]
def OrderIso.divLeft (a : α) : α ≃o αᵒᵈ where
  toEquiv := (Equiv.divLeft a).trans OrderDual.toDual
  map_rel_iff' {_ _} := div_le_div_iff_left (α := α) _

Order-reversing isomorphism $ x \mapsto a / x $

Informal description

For an element $ a $ in an ordered group $ \alpha $, the function $ x \mapsto a / x $ is an order-reversing isomorphism from $ \alpha $ to its order dual $ \alpha^{\text{op}} $. This means it is a bijective function that reverses the order relation: for any $ x, y \in \alpha $, we have $ x \leq y $ if and only if $ a / y \leq a / x $.

OrderIso.mulRight definition

(a : α) : α ≃o α

Full source

/-- `Equiv.mulRight` as an `OrderIso`. See also `OrderEmbedding.mulRight`. -/
@[to_additive (attr := simps! +simpRhs toEquiv apply)
  "`Equiv.addRight` as an `OrderIso`. See also `OrderEmbedding.addRight`."]
def OrderIso.mulRight (a : α) : α ≃o α where
  map_rel_iff' {_ _} := mul_le_mul_iff_right a
  toEquiv := Equiv.mulRight a

Order isomorphism induced by right multiplication

Informal description

For an element $a$ in an ordered group $\alpha$, the function $x \mapsto x * a$ is an order isomorphism from $\alpha$ to itself. This means it is a bijective function that preserves the order relation: for any $x, y \in \alpha$, we have $x \leq y$ if and only if $x * a \leq y * a$.

OrderIso.mulRight_symm theorem

(a : α) : (OrderIso.mulRight a).symm = OrderIso.mulRight a⁻¹

Full source

@[to_additive (attr := simp)]
theorem OrderIso.mulRight_symm (a : α) : (OrderIso.mulRight a).symm = OrderIso.mulRight a⁻¹ := by
  ext x
  rfl

Inverse of Right Multiplication Order Isomorphism Equals Right Multiplication by Inverse

Informal description

For any element $a$ in an ordered group $\alpha$, the inverse of the order isomorphism $x \mapsto x * a$ is equal to the order isomorphism $x \mapsto x * a^{-1}$.

OrderIso.divRight definition

(a : α) : α ≃o α

Full source

/-- `x ↦ x / a` as an order isomorphism. -/
@[to_additive (attr := simps!) "`x ↦ x - a` as an order isomorphism."]
def OrderIso.divRight (a : α) : α ≃o α where
  toEquiv := Equiv.divRight a
  map_rel_iff' {_ _} := div_le_div_iff_right a

Order isomorphism induced by right division

Informal description

For an element $a$ in an ordered group $\alpha$, the function $x \mapsto x / a$ is an order isomorphism from $\alpha$ to itself. This means it is a bijective function that preserves the order relation: for any $x, y \in \alpha$, we have $x \leq y$ if and only if $x / a \leq y / a$.

OrderIso.mulLeft definition

(a : α) : α ≃o α

Full source

/-- `Equiv.mulLeft` as an `OrderIso`. See also `OrderEmbedding.mulLeft`. -/
@[to_additive (attr := simps! +simpRhs toEquiv apply)
  "`Equiv.addLeft` as an `OrderIso`. See also `OrderEmbedding.addLeft`."]
def OrderIso.mulLeft (a : α) : α ≃o α where
  map_rel_iff' {_ _} := mul_le_mul_iff_left a
  toEquiv := Equiv.mulLeft a

Order isomorphism induced by left multiplication

Informal description

For an element $ a $ in an ordered group $ \alpha $, the function $ x \mapsto a * x $ is an order isomorphism from $ \alpha $ to itself. This means it is a bijective function that preserves the order relation: for any $ x, y \in \alpha $, we have $ x \leq y $ if and only if $ a * x \leq a * y $.

OrderIso.mulLeft_symm theorem

(a : α) : (OrderIso.mulLeft a).symm = OrderIso.mulLeft a⁻¹

Full source

@[to_additive (attr := simp)]
theorem OrderIso.mulLeft_symm (a : α) : (OrderIso.mulLeft a).symm = OrderIso.mulLeft a⁻¹ := by
  ext x
  rfl

Inverse of Left Multiplication Order Isomorphism in Ordered Groups

Informal description

For any element $a$ in an ordered group $\alpha$, the inverse of the order isomorphism $x \mapsto a * x$ is equal to the order isomorphism $x \mapsto a^{-1} * x$. In other words, $(\text{OrderIso.mulLeft}\, a)^{-1} = \text{OrderIso.mulLeft}\, a^{-1}$.