Documentation

Mathlib.Algebra.Order.Group.Opposite

Order instances for MulOpposite/AddOpposite #

This files transfers order instances and ordered monoid/group instances from α to αᵐᵒᵖ and αᵃᵒᵖ.

source
instance MulOpposite.instPreorder {α : Type u_1} [Preorder α] :
Preorder αᵐᵒᵖ
Equations
    source
    instance AddOpposite.instPreorder {α : Type u_1} [Preorder α] :
    Preorder αᵃᵒᵖ
    Equations
      source
      @[simp]
      theorem MulOpposite.unop_le_unop {α : Type u_1} [Preorder α] {a b : αᵐᵒᵖ} :
      unop a ≤ unop b ↔ a ≤ b
      source
      @[simp]
      theorem AddOpposite.unop_le_unop {α : Type u_1} [Preorder α] {a b : αᵃᵒᵖ} :
      unop a ≤ unop b ↔ a ≤ b
      source
      @[simp]
      theorem MulOpposite.op_le_op {α : Type u_1} [Preorder α] {a b : α} :
      op a ≤ op b ↔ a ≤ b
      source
      @[simp]
      theorem AddOpposite.op_le_op {α : Type u_1} [Preorder α] {a b : α} :
      op a ≤ op b ↔ a ≤ b
      source
      instance MulOpposite.instPartialOrder {α : Type u_1} [PartialOrder α] :
      PartialOrder αᵐᵒᵖ
      Equations
        source
        instance AddOpposite.instPartialOrder {α : Type u_1} [PartialOrder α] :
        PartialOrder αᵃᵒᵖ
        Equations
          source
          instance MulOpposite.instIsOrderedMonoid {α : Type u_1} [CommMonoid α] [PartialOrder α] [IsOrderedMonoid α] :
          IsOrderedMonoid αᵐᵒᵖ
          source
          instance AddOpposite.instIsOrderedAddMonoid {α : Type u_1} [AddCommMonoid α] [PartialOrder α] [IsOrderedAddMonoid α] :
          IsOrderedAddMonoid αᵃᵒᵖ
          source
          @[simp]
          theorem MulOpposite.unop_le_one {α : Type u_1} [CommMonoid α] [PartialOrder α] {a : αᵐᵒᵖ} :
          unop a ≤ 1 ↔ a ≤ 1
          source
          @[simp]
          theorem AddOpposite.unop_nonpos {α : Type u_1} [AddCommMonoid α] [PartialOrder α] {a : αᵃᵒᵖ} :
          unop a ≤ 0 ↔ a ≤ 0
          source
          @[simp]
          theorem MulOpposite.one_le_unop {α : Type u_1} [CommMonoid α] [PartialOrder α] {a : αᵐᵒᵖ} :
          1 ≤ unop a ↔ 1 ≤ a
          source
          @[simp]
          theorem AddOpposite.nonneg_unop {α : Type u_1} [AddCommMonoid α] [PartialOrder α] {a : αᵃᵒᵖ} :
          0 ≤ unop a ↔ 0 ≤ a
          source
          @[simp]
          theorem MulOpposite.op_le_one {α : Type u_1} [CommMonoid α] [PartialOrder α] {a : α} :
          op a ≤ 1 ↔ a ≤ 1
          source
          @[simp]
          theorem AddOpposite.op_nonpos {α : Type u_1} [AddCommMonoid α] [PartialOrder α] {a : α} :
          op a ≤ 0 ↔ a ≤ 0
          source
          @[simp]
          theorem MulOpposite.one_le_op {α : Type u_1} [CommMonoid α] [PartialOrder α] {a : α} :
          1 ≤ op a ↔ 1 ≤ a
          source
          @[simp]
          theorem AddOpposite.nonneg_op {α : Type u_1} [AddCommMonoid α] [PartialOrder α] {a : α} :
          0 ≤ op a ↔ 0 ≤ a
          source
          instance MulOpposite.instIsOrderedAddMonoid {α : Type u_1} [AddCommMonoid α] [PartialOrder α] [IsOrderedAddMonoid α] :
          IsOrderedAddMonoid αᵐᵒᵖ
          source
          @[simp]
          theorem MulOpposite.unop_nonpos {α : Type u_1} [AddCommMonoid α] [PartialOrder α] {a : αᵐᵒᵖ} :
          unop a ≤ 0 ↔ a ≤ 0
          source
          @[simp]
          theorem MulOpposite.unop_nonneg {α : Type u_1} [AddCommMonoid α] [PartialOrder α] {a : αᵐᵒᵖ} :
          0 ≤ unop a ↔ 0 ≤ a
          source
          @[simp]
          theorem MulOpposite.op_nonpos {α : Type u_1} [AddCommMonoid α] [PartialOrder α] {a : α} :
          op a ≤ 0 ↔ a ≤ 0
          source
          @[simp]
          theorem MulOpposite.op_nonneg {α : Type u_1} [AddCommMonoid α] [PartialOrder α] {a : α} :
          0 ≤ op a ↔ 0 ≤ a
          source
          instance AddOpposite.instIsOrderedMonoid {α : Type u_1} [CommMonoid α] [PartialOrder α] [IsOrderedMonoid α] :
          IsOrderedMonoid αᵃᵒᵖ
          source
          @[simp]
          theorem AddOpposite.unop_le_one {α : Type u_1} [CommMonoid α] [PartialOrder α] {a : αᵃᵒᵖ} :
          unop a ≤ 1 ↔ a ≤ 1
          source
          @[simp]
          theorem AddOpposite.one_le_unop {α : Type u_1} [CommMonoid α] [PartialOrder α] {a : αᵃᵒᵖ} :
          1 ≤ unop a ↔ 1 ≤ a
          source
          @[simp]
          theorem AddOpposite.op_le_one {α : Type u_1} [CommMonoid α] [PartialOrder α] {a : α} :
          op a ≤ 1 ↔ a ≤ 1
          source
          @[simp]
          theorem AddOpposite.one_le_op {α : Type u_1} [CommMonoid α] [PartialOrder α] {a : α} :
          1 ≤ op a ↔ 1 ≤ a