Inverse and multiplication as order isomorphisms in ordered groups

def OrderIso.neg (α : Type u) [AddGroup α] [LE α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 ≤ x2] [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 ≤ x2] : α ≃o αᵒᵈ

x ↦ -x as an order-reversing equivalence.

Equations

• OrderIso.neg α = { toEquiv := Equiv.trans (Equiv.neg α) OrderDual.toDual, map_rel_iff' := ⋯ }

@[simp]

theorem OrderIso.neg_symm_apply (α : Type u) [AddGroup α] [LE α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 ≤ x2] [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 ≤ x2] : ∀ (a : αᵒᵈ), (RelIso.symm (OrderIso.neg α)) a = -OrderDual.ofDual a

@[simp]

theorem OrderIso.inv_apply (α : Type u) [Group α] [LE α] [CovariantClass α α (fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 ≤ x2] [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 ≤ x2] : ∀ (a : α), (OrderIso.inv α) a = OrderDual.toDual a⁻¹

@[simp]

theorem OrderIso.inv_symm_apply (α : Type u) [Group α] [LE α] [CovariantClass α α (fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 ≤ x2] [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 ≤ x2] : ∀ (a : αᵒᵈ), (RelIso.symm (OrderIso.inv α)) a = (OrderDual.ofDual a)⁻¹

@[simp]

theorem OrderIso.neg_apply (α : Type u) [AddGroup α] [LE α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 ≤ x2] [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 ≤ x2] : ∀ (a : α), (OrderIso.neg α) a = OrderDual.toDual (-a)

def OrderIso.inv (α : Type u) [Group α] [LE α] [CovariantClass α α (fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 ≤ x2] [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 ≤ x2] : α ≃o αᵒᵈ

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

Equations

• OrderIso.inv α = { toEquiv := Equiv.trans (Equiv.inv α) OrderDual.toDual, map_rel_iff' := ⋯ }

theorem neg_le {α : Type u} [AddGroup α] [LE α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 ≤ x2] [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 ≤ x2] {a : α} {b : α} : -a ≤ b ↔ -b ≤ a

theorem inv_le' {α : Type u} [Group α] [LE α] [CovariantClass α α (fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 ≤ x2] [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 ≤ x2] {a : α} {b : α} : a⁻¹ ≤ b ↔ b⁻¹ ≤ a

theorem inv_le_of_inv_le' {α : Type u} [Group α] [LE α] [CovariantClass α α (fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 ≤ x2] [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 ≤ x2] {a : α} {b : α} : a⁻¹ ≤ b → b⁻¹ ≤ a

Alias of the forward direction of inv_le'.

theorem neg_le_of_neg_le {α : Type u} [AddGroup α] [LE α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 ≤ x2] [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 ≤ x2] {a : α} {b : α} : -a ≤ b → -b ≤ a

theorem le_neg {α : Type u} [AddGroup α] [LE α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 ≤ x2] [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 ≤ x2] {a : α} {b : α} : a ≤ -b ↔ b ≤ -a

theorem le_inv' {α : Type u} [Group α] [LE α] [CovariantClass α α (fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 ≤ x2] [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 ≤ x2] {a : α} {b : α} : a ≤ b⁻¹ ↔ b ≤ a⁻¹

def OrderIso.subLeft {α : Type u} [AddGroup α] [LE α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 ≤ x2] [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 ≤ x2] (a : α) : α ≃o αᵒᵈ

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

Equations

• OrderIso.subLeft a = { toEquiv := (Equiv.subLeft a).trans OrderDual.toDual, map_rel_iff' := ⋯ }

@[simp]

theorem OrderIso.subLeft_symm_apply {α : Type u} [AddGroup α] [LE α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 ≤ x2] [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 ≤ x2] (a : α) : ∀ (a_1 : αᵒᵈ), (RelIso.symm (OrderIso.subLeft a)) a_1 = -OrderDual.ofDual a_1 + a

@[simp]

theorem OrderIso.divLeft_apply {α : Type u} [Group α] [LE α] [CovariantClass α α (fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 ≤ x2] [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 ≤ x2] (a : α) : ∀ (a_1 : α), (OrderIso.divLeft a) a_1 = OrderDual.toDual (a / a_1)

@[simp]

theorem OrderIso.subLeft_apply {α : Type u} [AddGroup α] [LE α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 ≤ x2] [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 ≤ x2] (a : α) : ∀ (a_1 : α), (OrderIso.subLeft a) a_1 = OrderDual.toDual (a - a_1)

@[simp]

theorem OrderIso.divLeft_symm_apply {α : Type u} [Group α] [LE α] [CovariantClass α α (fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 ≤ x2] [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 ≤ x2] (a : α) : ∀ (a_1 : αᵒᵈ), (RelIso.symm (OrderIso.divLeft a)) a_1 = (OrderDual.ofDual a_1)⁻¹ * a

def OrderIso.divLeft {α : Type u} [Group α] [LE α] [CovariantClass α α (fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 ≤ x2] [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 ≤ x2] (a : α) : α ≃o αᵒᵈ

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

Equations

• OrderIso.divLeft a = { toEquiv := (Equiv.divLeft a).trans OrderDual.toDual, map_rel_iff' := ⋯ }

theorem le_inv_of_le_inv {α : Type u} [Group α] [LE α] [CovariantClass α α (fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 ≤ x2] [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 ≤ x2] {a : α} {b : α} : a ≤ b⁻¹ → b ≤ a⁻¹

Alias of the forward direction of le_inv'.

theorem le_neg_of_le_neg {α : Type u} [AddGroup α] [LE α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 ≤ x2] [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 ≤ x2] {a : α} {b : α} : a ≤ -b → b ≤ -a

theorem OrderIso.addRight.proof_1 {α : Type u_1} [AddGroup α] [LE α] [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 ≤ x2] (a : α) : ∀ {x x_1 : α}, x + a ≤ x_1 + a ↔ x ≤ x_1

def OrderIso.addRight {α : Type u} [AddGroup α] [LE α] [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 ≤ x2] (a : α) : α ≃o α

Equiv.addRight as an OrderIso. See also OrderEmbedding.addRight.

Equations

• OrderIso.addRight a = { toEquiv := Equiv.addRight a, map_rel_iff' := ⋯ }

@[simp]

theorem OrderIso.mulRight_apply {α : Type u} [Group α] [LE α] [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 ≤ x2] (a : α) (x : α) : (OrderIso.mulRight a) x = x * a

@[simp]

theorem OrderIso.addRight_toEquiv {α : Type u} [AddGroup α] [LE α] [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 ≤ x2] (a : α) : (OrderIso.addRight a).toEquiv = Equiv.addRight a

@[simp]

theorem OrderIso.addRight_apply {α : Type u} [AddGroup α] [LE α] [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 ≤ x2] (a : α) (x : α) : (OrderIso.addRight a) x = x + a

@[simp]

theorem OrderIso.mulRight_toEquiv {α : Type u} [Group α] [LE α] [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 ≤ x2] (a : α) : (OrderIso.mulRight a).toEquiv = Equiv.mulRight a

def OrderIso.mulRight {α : Type u} [Group α] [LE α] [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 ≤ x2] (a : α) : α ≃o α

Equiv.mulRight as an OrderIso. See also OrderEmbedding.mulRight.

Equations

• OrderIso.mulRight a = { toEquiv := Equiv.mulRight a, map_rel_iff' := ⋯ }

@[simp]

theorem OrderIso.addRight_symm {α : Type u} [AddGroup α] [LE α] [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 ≤ x2] (a : α) : (OrderIso.addRight a).symm = OrderIso.addRight (-a)

@[simp]

theorem OrderIso.mulRight_symm {α : Type u} [Group α] [LE α] [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 ≤ x2] (a : α) : (OrderIso.mulRight a).symm = OrderIso.mulRight a⁻¹

def OrderIso.subRight {α : Type u} [AddGroup α] [LE α] [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 ≤ x2] (a : α) : α ≃o α

x ↦ x - a as an order isomorphism.

Equations

• OrderIso.subRight a = { toEquiv := Equiv.subRight a, map_rel_iff' := ⋯ }

@[simp]

theorem OrderIso.subRight_apply {α : Type u} [AddGroup α] [LE α] [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 ≤ x2] (a : α) (b : α) : (OrderIso.subRight a) b = b - a

@[simp]

theorem OrderIso.divRight_apply {α : Type u} [Group α] [LE α] [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 ≤ x2] (a : α) (b : α) : (OrderIso.divRight a) b = b / a

@[simp]

theorem OrderIso.subRight_symm_apply {α : Type u} [AddGroup α] [LE α] [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 ≤ x2] (a : α) (b : α) : (RelIso.symm (OrderIso.subRight a)) b = b + a

@[simp]

theorem OrderIso.divRight_symm_apply {α : Type u} [Group α] [LE α] [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 ≤ x2] (a : α) (b : α) : (RelIso.symm (OrderIso.divRight a)) b = b * a

def OrderIso.divRight {α : Type u} [Group α] [LE α] [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 ≤ x2] (a : α) : α ≃o α

x ↦ x / a as an order isomorphism.

Equations

• OrderIso.divRight a = { toEquiv := Equiv.divRight a, map_rel_iff' := ⋯ }

def OrderIso.addLeft {α : Type u} [AddGroup α] [LE α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 ≤ x2] (a : α) : α ≃o α

Equiv.addLeft as an OrderIso. See also OrderEmbedding.addLeft.

Equations

• OrderIso.addLeft a = { toEquiv := Equiv.addLeft a, map_rel_iff' := ⋯ }

theorem OrderIso.addLeft.proof_1 {α : Type u_1} [AddGroup α] [LE α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 ≤ x2] (a : α) : ∀ {x x_1 : α}, a + x ≤ a + x_1 ↔ x ≤ x_1

@[simp]

theorem OrderIso.mulLeft_apply {α : Type u} [Group α] [LE α] [CovariantClass α α (fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 ≤ x2] (a : α) (x : α) : (OrderIso.mulLeft a) x = a * x

@[simp]

theorem OrderIso.addLeft_toEquiv {α : Type u} [AddGroup α] [LE α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 ≤ x2] (a : α) : (OrderIso.addLeft a).toEquiv = Equiv.addLeft a

@[simp]

theorem OrderIso.mulLeft_toEquiv {α : Type u} [Group α] [LE α] [CovariantClass α α (fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 ≤ x2] (a : α) : (OrderIso.mulLeft a).toEquiv = Equiv.mulLeft a

@[simp]

theorem OrderIso.addLeft_apply {α : Type u} [AddGroup α] [LE α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 ≤ x2] (a : α) (x : α) : (OrderIso.addLeft a) x = a + x

def OrderIso.mulLeft {α : Type u} [Group α] [LE α] [CovariantClass α α (fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 ≤ x2] (a : α) : α ≃o α

Equiv.mulLeft as an OrderIso. See also OrderEmbedding.mulLeft.

Equations

• OrderIso.mulLeft a = { toEquiv := Equiv.mulLeft a, map_rel_iff' := ⋯ }

@[simp]

theorem OrderIso.addLeft_symm {α : Type u} [AddGroup α] [LE α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 ≤ x2] (a : α) : (OrderIso.addLeft a).symm = OrderIso.addLeft (-a)

@[simp]

theorem OrderIso.mulLeft_symm {α : Type u} [Group α] [LE α] [CovariantClass α α (fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 ≤ x2] (a : α) : (OrderIso.mulLeft a).symm = OrderIso.mulLeft a⁻¹