Inverse and multiplication as order isomorphisms in ordered groups #
def
OrderIso.neg
(α : Type u)
[inst : AddGroup α]
[inst : LE α]
[inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1]
[inst : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1]
:
x ↦ -x
as an order-reversing equivalence.
Equations
- OrderIso.neg α = { toEquiv := Equiv.trans (Equiv.neg α) OrderDual.toDual, map_rel_iff' := (_ : ∀ {x x_1 : α}, -x_1 ≤ -x ↔ x ≤ x_1) }
def
OrderIso.neg.proof_1
(α : Type u_1)
[inst : AddGroup α]
[inst : LE α]
[inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1]
[inst : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1]
:
@[simp]
theorem
OrderIso.neg_symm_apply
(α : Type u)
[inst : AddGroup α]
[inst : LE α]
[inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1]
[inst : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1]
:
∀ (a : αᵒᵈ), ↑(RelIso.toRelEmbedding (RelIso.symm (OrderIso.neg α))).toEmbedding a = -↑OrderDual.ofDual a
@[simp]
theorem
OrderIso.inv_apply
(α : Type u)
[inst : Group α]
[inst : LE α]
[inst : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1]
[inst : CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1]
:
∀ (a : α), ↑(RelIso.toRelEmbedding (OrderIso.inv α)).toEmbedding a = ↑OrderDual.toDual a⁻¹
@[simp]
theorem
OrderIso.neg_apply
(α : Type u)
[inst : AddGroup α]
[inst : LE α]
[inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1]
[inst : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1]
:
∀ (a : α), ↑(RelIso.toRelEmbedding (OrderIso.neg α)).toEmbedding a = ↑OrderDual.toDual (-a)
@[simp]
theorem
OrderIso.inv_symm_apply
(α : Type u)
[inst : Group α]
[inst : LE α]
[inst : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1]
[inst : CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1]
:
∀ (a : αᵒᵈ), ↑(RelIso.toRelEmbedding (RelIso.symm (OrderIso.inv α))).toEmbedding a = (↑OrderDual.ofDual a)⁻¹
def
OrderIso.inv
(α : Type u)
[inst : Group α]
[inst : LE α]
[inst : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1]
[inst : CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1]
:
x ↦ x⁻¹
as an order-reversing equivalence.
Equations
- OrderIso.inv α = { toEquiv := Equiv.trans (Equiv.inv α) OrderDual.toDual, map_rel_iff' := (_ : ∀ {x x_1 : α}, x_1⁻¹ ≤ x⁻¹ ↔ x ≤ x_1) }
theorem
inv_le_of_inv_le'
{α : Type u}
[inst : Group α]
[inst : LE α]
[inst : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1]
[inst : CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1]
{a : α}
{b : α}
:
Alias of the forward direction of inv_le'
.
theorem
neg_le_of_neg_le
{α : Type u}
[inst : AddGroup α]
[inst : LE α]
[inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1]
[inst : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1]
{a : α}
{b : α}
:
theorem
le_inv_of_le_inv
{α : Type u}
[inst : Group α]
[inst : LE α]
[inst : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1]
[inst : CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1]
{a : α}
{b : α}
:
Alias of the forward direction of le_inv'
.
theorem
le_neg_of_le_neg
{α : Type u}
[inst : AddGroup α]
[inst : LE α]
[inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1]
[inst : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1]
{a : α}
{b : α}
:
def
OrderIso.addRight
{α : Type u}
[inst : AddGroup α]
[inst : LE α]
[inst : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1]
(a : α)
:
α ≃o α
Equiv.addRight
as an OrderIso
. See also OrderEmbedding.addRight
.
Equations
- OrderIso.addRight a = { toEquiv := Equiv.addRight a, map_rel_iff' := (_ : ∀ {x x_1 : α}, x + a ≤ x_1 + a ↔ x ≤ x_1) }
@[simp]
theorem
OrderIso.addRight_apply
{α : Type u}
[inst : AddGroup α]
[inst : LE α]
[inst : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1]
(a : α)
(x : α)
:
↑(RelIso.toRelEmbedding (OrderIso.addRight a)).toEmbedding x = x + a
@[simp]
theorem
OrderIso.addRight_toEquiv
{α : Type u}
[inst : AddGroup α]
[inst : LE α]
[inst : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1]
(a : α)
:
(OrderIso.addRight a).toEquiv = Equiv.addRight a
@[simp]
theorem
OrderIso.mulRight_toEquiv
{α : Type u}
[inst : Group α]
[inst : LE α]
[inst : CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1]
(a : α)
:
(OrderIso.mulRight a).toEquiv = Equiv.mulRight a
@[simp]
theorem
OrderIso.mulRight_apply
{α : Type u}
[inst : Group α]
[inst : LE α]
[inst : CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1]
(a : α)
(x : α)
:
↑(RelIso.toRelEmbedding (OrderIso.mulRight a)).toEmbedding x = x * a
def
OrderIso.mulRight
{α : Type u}
[inst : Group α]
[inst : LE α]
[inst : CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1]
(a : α)
:
α ≃o α
Equiv.mulRight
as an OrderIso
. See also OrderEmbedding.mulRight
.
Equations
- OrderIso.mulRight a = { toEquiv := Equiv.mulRight a, map_rel_iff' := (_ : ∀ {x x_1 : α}, x * a ≤ x_1 * a ↔ x ≤ x_1) }
@[simp]
theorem
OrderIso.addRight_symm
{α : Type u}
[inst : AddGroup α]
[inst : LE α]
[inst : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1]
(a : α)
:
@[simp]
theorem
OrderIso.mulRight_symm
{α : Type u}
[inst : Group α]
[inst : LE α]
[inst : CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1]
(a : α)
:
def
OrderIso.addLeft
{α : Type u}
[inst : AddGroup α]
[inst : LE α]
[inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1]
(a : α)
:
α ≃o α
Equiv.addLeft
as an OrderIso
. See also OrderEmbedding.addLeft
.
Equations
- OrderIso.addLeft a = { toEquiv := Equiv.addLeft a, map_rel_iff' := (_ : ∀ {x x_1 : α}, a + x ≤ a + x_1 ↔ x ≤ x_1) }
@[simp]
theorem
OrderIso.addLeft_apply
{α : Type u}
[inst : AddGroup α]
[inst : LE α]
[inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1]
(a : α)
(x : α)
:
↑(RelIso.toRelEmbedding (OrderIso.addLeft a)).toEmbedding x = a + x
@[simp]
theorem
OrderIso.mulLeft_toEquiv
{α : Type u}
[inst : Group α]
[inst : LE α]
[inst : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1]
(a : α)
:
(OrderIso.mulLeft a).toEquiv = Equiv.mulLeft a
@[simp]
theorem
OrderIso.addLeft_toEquiv
{α : Type u}
[inst : AddGroup α]
[inst : LE α]
[inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1]
(a : α)
:
(OrderIso.addLeft a).toEquiv = Equiv.addLeft a
@[simp]
theorem
OrderIso.mulLeft_apply
{α : Type u}
[inst : Group α]
[inst : LE α]
[inst : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1]
(a : α)
(x : α)
:
↑(RelIso.toRelEmbedding (OrderIso.mulLeft a)).toEmbedding x = a * x
def
OrderIso.mulLeft
{α : Type u}
[inst : Group α]
[inst : LE α]
[inst : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1]
(a : α)
:
α ≃o α
Equiv.mulLeft
as an OrderIso
. See also OrderEmbedding.mulLeft
.
Equations
- OrderIso.mulLeft a = { toEquiv := Equiv.mulLeft a, map_rel_iff' := (_ : ∀ {x x_1 : α}, a * x ≤ a * x_1 ↔ x ≤ x_1) }
@[simp]
theorem
OrderIso.addLeft_symm
{α : Type u}
[inst : AddGroup α]
[inst : LE α]
[inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1]
(a : α)
:
@[simp]
theorem
OrderIso.mulLeft_symm
{α : Type u}
[inst : Group α]
[inst : LE α]
[inst : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1]
(a : α)
: