Theorems · Definition · order theory
OrderIso.subLeft
{α : Type u} → [inst : AddGroup α] → [inst_1 : LE α] → [AddLeftMono α] → [AddRightMono α] → α → α ≃o αᵒᵈx ↦ a - x as an order-reversing equivalence.
- Defined in
- Mathlib.Algebra.Order.Group.OrderIso
- Cited by
- 4 results in Mathlib
- Foundations
- Depth 16 from the axioms · uses propext, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites10
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Equivproof · cited by 8,337
- AddGroupstatement and proof · cited by 4,410
- OrderDualstatement and proof · cited by 927
- OrderIsostatement · cited by 874
- AddLeftMonostatement and proof · cited by 687
- OrderDual.toDualproof · cited by 481
- AddRightMonostatement and proof · cited by 367
- Equiv.transproof · cited by 337
- Equiv.subLeftproof · cited by 10
- sub_le_sub_iff_leftproof · cited by 8
Cited by4
Results whose statement or proof uses this declaration.
- sub_infproof · cited by 1
- sub_supproof · cited by 1
- OrderIso.subLeft_applystatement and proof · cited by 0
- OrderIso.subLeft_symm_applystatement and proof · cited by 0