Order instances for MulOpposite/AddOpposite

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

instance MulOpposite.instPreorder {α : Type u_1} [Preorder α] : Preorder αᵐᵒᵖ

Equations

• MulOpposite.instPreorder = Preorder.lift MulOpposite.unop

instance AddOpposite.instPreorder {α : Type u_1} [Preorder α] : Preorder αᵃᵒᵖ

Equations

• AddOpposite.instPreorder = Preorder.lift AddOpposite.unop

@[simp]

theorem MulOpposite.unop_le_unop {α : Type u_1} [Preorder α] {a b : αᵐᵒᵖ} : unop a ≤ unop b ↔ a ≤ b

@[simp]

theorem AddOpposite.unop_le_unop {α : Type u_1} [Preorder α] {a b : αᵃᵒᵖ} : unop a ≤ unop b ↔ a ≤ b

@[simp]

theorem MulOpposite.op_le_op {α : Type u_1} [Preorder α] {a b : α} : op a ≤ op b ↔ a ≤ b

@[simp]

theorem AddOpposite.op_le_op {α : Type u_1} [Preorder α] {a b : α} : op a ≤ op b ↔ a ≤ b

instance MulOpposite.instPartialOrder {α : Type u_1} [PartialOrder α] : PartialOrder αᵐᵒᵖ

Equations

• MulOpposite.instPartialOrder = PartialOrder.lift MulOpposite.unop ⋯

instance AddOpposite.instPartialOrder {α : Type u_1} [PartialOrder α] : PartialOrder αᵃᵒᵖ

Equations

• AddOpposite.instPartialOrder = PartialOrder.lift AddOpposite.unop ⋯

instance MulOpposite.instIsOrderedMonoid {α : Type u_1} [CommMonoid α] [PartialOrder α] [IsOrderedMonoid α] : IsOrderedMonoid αᵐᵒᵖ

instance AddOpposite.instIsOrderedAddMonoid {α : Type u_1} [AddCommMonoid α] [PartialOrder α] [IsOrderedAddMonoid α] : IsOrderedAddMonoid αᵃᵒᵖ

@[simp]

theorem MulOpposite.unop_le_one {α : Type u_1} [CommMonoid α] [PartialOrder α] {a : αᵐᵒᵖ} : unop a ≤ 1 ↔ a ≤ 1

@[simp]

theorem AddOpposite.unop_nonpos {α : Type u_1} [AddCommMonoid α] [PartialOrder α] {a : αᵃᵒᵖ} : unop a ≤ 0 ↔ a ≤ 0

@[simp]

theorem MulOpposite.one_le_unop {α : Type u_1} [CommMonoid α] [PartialOrder α] {a : αᵐᵒᵖ} : 1 ≤ unop a ↔ 1 ≤ a

@[simp]

theorem AddOpposite.nonneg_unop {α : Type u_1} [AddCommMonoid α] [PartialOrder α] {a : αᵃᵒᵖ} : 0 ≤ unop a ↔ 0 ≤ a

@[simp]

theorem MulOpposite.op_le_one {α : Type u_1} [CommMonoid α] [PartialOrder α] {a : α} : op a ≤ 1 ↔ a ≤ 1

@[simp]

theorem AddOpposite.op_nonpos {α : Type u_1} [AddCommMonoid α] [PartialOrder α] {a : α} : op a ≤ 0 ↔ a ≤ 0

@[simp]

theorem MulOpposite.one_le_op {α : Type u_1} [CommMonoid α] [PartialOrder α] {a : α} : 1 ≤ op a ↔ 1 ≤ a

@[simp]

theorem AddOpposite.nonneg_op {α : Type u_1} [AddCommMonoid α] [PartialOrder α] {a : α} : 0 ≤ op a ↔ 0 ≤ a

instance MulOpposite.instIsOrderedAddMonoid {α : Type u_1} [AddCommMonoid α] [PartialOrder α] [IsOrderedAddMonoid α] : IsOrderedAddMonoid αᵐᵒᵖ

@[simp]

theorem MulOpposite.unop_nonpos {α : Type u_1} [AddCommMonoid α] [PartialOrder α] {a : αᵐᵒᵖ} : unop a ≤ 0 ↔ a ≤ 0

@[simp]

theorem MulOpposite.unop_nonneg {α : Type u_1} [AddCommMonoid α] [PartialOrder α] {a : αᵐᵒᵖ} : 0 ≤ unop a ↔ 0 ≤ a

@[simp]

theorem MulOpposite.op_nonpos {α : Type u_1} [AddCommMonoid α] [PartialOrder α] {a : α} : op a ≤ 0 ↔ a ≤ 0

@[simp]

theorem MulOpposite.op_nonneg {α : Type u_1} [AddCommMonoid α] [PartialOrder α] {a : α} : 0 ≤ op a ↔ 0 ≤ a

instance AddOpposite.instIsOrderedMonoid {α : Type u_1} [CommMonoid α] [PartialOrder α] [IsOrderedMonoid α] : IsOrderedMonoid αᵃᵒᵖ

@[simp]

theorem AddOpposite.unop_le_one {α : Type u_1} [CommMonoid α] [PartialOrder α] {a : αᵃᵒᵖ} : unop a ≤ 1 ↔ a ≤ 1

@[simp]

theorem AddOpposite.one_le_unop {α : Type u_1} [CommMonoid α] [PartialOrder α] {a : αᵃᵒᵖ} : 1 ≤ unop a ↔ 1 ≤ a

@[simp]

theorem AddOpposite.op_le_one {α : Type u_1} [CommMonoid α] [PartialOrder α] {a : α} : op a ≤ 1 ↔ a ≤ 1

@[simp]

theorem AddOpposite.one_le_op {α : Type u_1} [CommMonoid α] [PartialOrder α] {a : α} : 1 ≤ op a ↔ 1 ≤ a