Documentation

Mathlib.Algebra.Order.Group.OrderIso

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] :

x ↦ -x as an order-reversing equivalence.

Equations
Instances For
    @[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] :

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

    Equations
    Instances For
      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 : α} :
      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⁻¹ bb⁻¹ 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 : α} :
      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 : α) :

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

      Equations
      Instances For
        @[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 : α) :

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

        Equations
        Instances For
          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 -bb -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
          Instances For
            @[simp]
            theorem OrderIso.mulRight_apply {α : Type u} [Group α] [LE α] [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 x2] (a : α) (x : α) :
            @[simp]
            theorem OrderIso.addRight_toEquiv {α : Type u} [AddGroup α] [LE α] [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 x2] (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 : α) :
            @[simp]
            theorem OrderIso.mulRight_toEquiv {α : Type u} [Group α] [LE α] [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 x2] (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
            Instances For
              @[simp]
              theorem OrderIso.addRight_symm {α : Type u} [AddGroup α] [LE α] [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 x2] (a : α) :
              @[simp]
              theorem OrderIso.mulRight_symm {α : Type u} [Group α] [LE α] [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 x2] (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
              Instances For
                @[simp]
                theorem OrderIso.subRight_apply {α : Type u} [AddGroup α] [LE α] [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 x2] (a : α) (b : α) :
                @[simp]
                theorem OrderIso.divRight_apply {α : Type u} [Group α] [LE α] [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 x2] (a : α) (b : α) :
                @[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 : α) :
                @[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 : α) :
                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
                Instances For
                  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
                  Instances For
                    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 : α) :
                    @[simp]
                    theorem OrderIso.mulLeft_toEquiv {α : Type u} [Group α] [LE α] [CovariantClass α α (fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 x2] (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
                    Instances For
                      @[simp]
                      theorem OrderIso.addLeft_symm {α : Type u} [AddGroup α] [LE α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 x2] (a : α) :
                      @[simp]
                      theorem OrderIso.mulLeft_symm {α : Type u} [Group α] [LE α] [CovariantClass α α (fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 x2] (a : α) :