Basic

📁 Source: Mathlib/Algebra/Order/Sub/Unbundled/Basic.lean

Statistics

Metric	Count
Definitions	0
Theorems `add_add_tsub_cancel`, `add_tsub_assoc_of_le`, `add_tsub_tsub_cancel`, `eq_tsub_iff_add_eq_of_le`, `le_tsub_iff_le_tsub`, `le_tsub_iff_left`, `le_tsub_iff_right`, `lt_of_tsub_lt_tsub_left_of_le`, `lt_tsub_iff_left_of_le`, `lt_tsub_iff_right_of_le`, `tsub_add_eq_add_tsub`, `tsub_add_tsub_comm`, `tsub_eq_iff_eq_add_of_le`, `tsub_inj_right`, `tsub_lt_iff_left`, `tsub_lt_iff_right`, `tsub_lt_iff_tsub_lt`, `tsub_lt_tsub_iff_left_of_le_of_le`, `tsub_lt_tsub_left_of_le`, `tsub_lt_tsub_right_of_le`, `tsub_tsub_assoc`, `tsub_tsub_cancel_of_le`, `tsub_tsub_tsub_cancel_left`, `add_add_tsub_cancel`, `add_le_of_le_tsub_left_of_le`, `add_le_of_le_tsub_right_of_le`, `add_tsub_assoc_of_le`, `add_tsub_cancel_of_le`, `add_tsub_tsub_cancel`, `eq_tsub_iff_add_eq_of_le`, `le_tsub_iff_le_tsub`, `le_tsub_iff_left`, `le_tsub_iff_right`, `lt_of_tsub_lt_tsub_left_of_le`, `lt_of_tsub_lt_tsub_right_of_le`, `lt_tsub_iff_left_of_le`, `lt_tsub_iff_right_of_le`, `tsub_add_cancel_of_le`, `tsub_add_eq_add_tsub`, `tsub_add_tsub_cancel`, `tsub_add_tsub_comm`, `tsub_eq_iff_eq_add_of_le`, `tsub_inj_left`, `tsub_inj_right`, `tsub_le_tsub_iff_right`, `tsub_left_inj`, `tsub_lt_iff_left`, `tsub_lt_iff_right`, `tsub_lt_iff_tsub_lt`, `tsub_lt_tsub_iff_left_of_le_of_le`, `tsub_lt_tsub_left_of_le`, `tsub_lt_tsub_right_of_le`, `tsub_tsub_assoc`, `tsub_tsub_cancel_of_le`, `tsub_tsub_eq_add_tsub_of_le`, `tsub_tsub_tsub_cancel_left`, `tsub_tsub_tsub_cancel_right`	57
Total	57

AddLECancellable

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`add_add_tsub_cancel` 📖	—	`AddLECancellable` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `Preorder.toLE` `PartialOrder.toPreorder`	—	—	`add_tsub_assoc_of_le` `add_right_comm` `add_tsub_cancel_right`
`add_tsub_assoc_of_le` 📖	—	`AddLECancellable` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `Preorder.toLE` `PartialOrder.toPreorder`	—	—	`add_tsub_cancel_of_le` `add_comm` `add_assoc` `add_tsub_cancel_right`
`add_tsub_tsub_cancel` 📖	—	`AddLECancellable` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `Preorder.toLE` `PartialOrder.toPreorder`	—	—	`tsub_eq_of_eq_add` `add_assoc` `add_tsub_cancel_of_le` `add_comm`
`eq_tsub_iff_add_eq_of_le` 📖	—	`AddLECancellable` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `Preorder.toLE` `PartialOrder.toPreorder`	—	—	`tsub_add_cancel_of_le` `eq_tsub_of_add_eq`
`le_tsub_iff_le_tsub` 📖	—	`AddLECancellable` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `Preorder.toLE` `PartialOrder.toPreorder`	—	—	`le_tsub_iff_left` `le_tsub_iff_right`
`le_tsub_iff_left` 📖	—	`AddLECancellable` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `Preorder.toLE` `PartialOrder.toPreorder`	—	—	`add_le_of_le_tsub_left_of_le` `le_tsub_of_add_le_left`
`le_tsub_iff_right` 📖	—	`AddLECancellable` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `Preorder.toLE` `PartialOrder.toPreorder`	—	—	`add_comm` `le_tsub_iff_left`
`lt_of_tsub_lt_tsub_left_of_le` 📖	—	`AddLECancellable` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `Preorder.toLE` `PartialOrder.toPreorder` `Preorder.toLT`	—	—	`lt_of_add_lt_add_left` `lt_add_of_tsub_lt_right` `tsub_add_cancel_of_le`
`lt_tsub_iff_left_of_le` 📖	mathematical	`AddLECancellable` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `Preorder.toLE` `PartialOrder.toPreorder`	`Preorder.toLT`	—	`add_comm` `lt_tsub_iff_right_of_le`
`lt_tsub_iff_right_of_le` 📖	mathematical	`AddLECancellable` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `Preorder.toLE` `PartialOrder.toPreorder`	`Preorder.toLT`	—	`LE.le.lt_of_ne` `add_le_of_le_tsub_right_of_le` `LT.lt.le` `LT.lt.ne'` `add_tsub_cancel_right` `lt_tsub_of_add_lt_right`
`tsub_add_eq_add_tsub` 📖	—	`AddLECancellable` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `Preorder.toLE` `PartialOrder.toPreorder`	—	—	`add_comm` `add_tsub_assoc_of_le`
`tsub_add_tsub_comm` 📖	—	`AddLECancellable` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `Preorder.toLE` `PartialOrder.toPreorder`	—	—	`tsub_add_eq_add_tsub` `add_tsub_assoc_of_le` `tsub_tsub` `add_comm`
`tsub_eq_iff_eq_add_of_le` 📖	—	`AddLECancellable` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `Preorder.toLE` `PartialOrder.toPreorder`	—	—	`eq_tsub_iff_add_eq_of_le`
`tsub_inj_right` 📖	—	`AddLECancellable` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `Preorder.toLE` `PartialOrder.toPreorder`	—	—	`tsub_add_cancel_of_le`
`tsub_lt_iff_left` 📖	mathematical	`AddLECancellable` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `Preorder.toLE` `PartialOrder.toPreorder`	`Preorder.toLT`	—	`lt_add_of_tsub_lt_left` `LE.le.lt_of_ne` `tsub_le_iff_left` `LT.lt.le` `LT.lt.ne'` `add_tsub_cancel_of_le`
`tsub_lt_iff_right` 📖	mathematical	`AddLECancellable` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `Preorder.toLE` `PartialOrder.toPreorder`	`Preorder.toLT`	—	`add_comm` `tsub_lt_iff_left`
`tsub_lt_iff_tsub_lt` 📖	mathematical	`AddLECancellable` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `Preorder.toLE` `PartialOrder.toPreorder`	`Preorder.toLT`	—	`tsub_lt_iff_left` `tsub_lt_iff_right`
`tsub_lt_tsub_iff_left_of_le_of_le` 📖	mathematical	`AddLECancellable` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `Preorder.toLE` `PartialOrder.toPreorder`	`Preorder.toLT`	—	`lt_of_tsub_lt_tsub_left_of_le` `tsub_lt_tsub_left_of_le`
`tsub_lt_tsub_left_of_le` 📖	—	`AddLECancellable` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `Preorder.toLE` `PartialOrder.toPreorder` `Preorder.toLT`	—	—	`LE.le.lt_of_ne` `tsub_le_tsub_left` `LT.lt.le` `LT.lt.ne'` `tsub_inj_right` `LE.le.trans`
`tsub_lt_tsub_right_of_le` 📖	—	`AddLECancellable` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `Preorder.toLE` `PartialOrder.toPreorder` `Preorder.toLT`	—	—	`lt_tsub_of_add_lt_left` `add_tsub_cancel_of_le`
`tsub_tsub_assoc` 📖	—	`AddLECancellable` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `Preorder.toLE` `PartialOrder.toPreorder`	—	—	`tsub_eq_of_eq_add` `add_assoc` `add_tsub_cancel_of_le` `tsub_add_cancel_of_le`
`tsub_tsub_cancel_of_le` 📖	—	`AddLECancellable` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `Preorder.toLE` `PartialOrder.toPreorder`	—	—	`tsub_eq_of_eq_add` `add_tsub_cancel_of_le`
`tsub_tsub_tsub_cancel_left` 📖	—	`AddLECancellable` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `Preorder.toLE` `PartialOrder.toPreorder`	—	—	`tsub_right_comm` `tsub_tsub_cancel_of_le`

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`add_add_tsub_cancel` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder`	`AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma`	—	`AddLECancellable.add_add_tsub_cancel` `Contravariant.AddLECancellable`
`add_le_of_le_tsub_left_of_le` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder`	`AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma`	—	`le_imp_le_of_le_of_le` `add_le_add_right` `le_refl` `add_tsub_cancel_of_le`
`add_le_of_le_tsub_right_of_le` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder`	`AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma`	—	`le_imp_le_of_le_of_le` `add_le_add_left` `covariant_swap_add_of_covariant_add` `le_refl` `tsub_add_cancel_of_le`
`add_tsub_assoc_of_le` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder`	`AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma`	—	`AddLECancellable.add_tsub_assoc_of_le` `Contravariant.AddLECancellable`
`add_tsub_cancel_of_le` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder`	`AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma`	—	`le_antisymm` `ExistsAddOfLE.exists_add_of_le` `le_imp_le_of_le_of_le` `add_le_add_right` `add_tsub_le_left` `le_refl` `le_add_tsub`
`add_tsub_tsub_cancel` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder`	`AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma`	—	`AddLECancellable.add_tsub_tsub_cancel` `Contravariant.AddLECancellable`
`eq_tsub_iff_add_eq_of_le` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder`	`AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma`	—	`AddLECancellable.eq_tsub_iff_add_eq_of_le` `Contravariant.AddLECancellable`
`le_tsub_iff_le_tsub` 📖	—	`Preorder.toLE` `PartialOrder.toPreorder`	—	—	`AddLECancellable.le_tsub_iff_le_tsub` `Contravariant.AddLECancellable`
`le_tsub_iff_left` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder`	`AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma`	—	`AddLECancellable.le_tsub_iff_left` `Contravariant.AddLECancellable`
`le_tsub_iff_right` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder`	`AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma`	—	`AddLECancellable.le_tsub_iff_right` `Contravariant.AddLECancellable`
`lt_of_tsub_lt_tsub_left_of_le` 📖	—	`Preorder.toLE` `PartialOrder.toPreorder` `Preorder.toLT`	—	—	`AddLECancellable.lt_of_tsub_lt_tsub_left_of_le` `Contravariant.AddLECancellable`
`lt_of_tsub_lt_tsub_right_of_le` 📖	—	`Preorder.toLE` `PartialOrder.toPreorder` `Preorder.toLT`	—	—	`LE.le.lt_of_ne` `tsub_le_tsub_iff_right` `LT.lt.le` `LT.lt.false`
`lt_tsub_iff_left_of_le` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder`	`Preorder.toLT` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma`	—	`AddLECancellable.lt_tsub_iff_left_of_le` `Contravariant.AddLECancellable`
`lt_tsub_iff_right_of_le` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder`	`Preorder.toLT` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma`	—	`AddLECancellable.lt_tsub_iff_right_of_le` `Contravariant.AddLECancellable`
`tsub_add_cancel_of_le` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder`	`AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma`	—	`add_comm` `add_tsub_cancel_of_le`
`tsub_add_eq_add_tsub` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder`	`AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma`	—	`AddLECancellable.tsub_add_eq_add_tsub` `Contravariant.AddLECancellable`
`tsub_add_tsub_cancel` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder`	`AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma`	—	`tsub_tsub` `add_tsub_cancel_of_le` `tsub_add_cancel_of_le` `tsub_le_tsub_right`
`tsub_add_tsub_comm` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder`	`AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma`	—	`AddLECancellable.tsub_add_tsub_comm` `Contravariant.AddLECancellable`
`tsub_eq_iff_eq_add_of_le` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder`	`AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma`	—	`AddLECancellable.tsub_eq_iff_eq_add_of_le` `Contravariant.AddLECancellable`
`tsub_inj_left` 📖	—	`Preorder.toLE` `PartialOrder.toPreorder`	—	—	—
`tsub_inj_right` 📖	—	`Preorder.toLE` `PartialOrder.toPreorder`	—	—	`AddLECancellable.tsub_inj_right` `Contravariant.AddLECancellable`
`tsub_le_tsub_iff_right` 📖	—	`Preorder.toLE` `PartialOrder.toPreorder`	—	—	`tsub_le_iff_right` `tsub_add_cancel_of_le`
`tsub_left_inj` 📖	—	`Preorder.toLE` `PartialOrder.toPreorder`	—	—	`tsub_le_tsub_iff_right`
`tsub_lt_iff_left` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder`	`Preorder.toLT` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma`	—	`AddLECancellable.tsub_lt_iff_left` `Contravariant.AddLECancellable`
`tsub_lt_iff_right` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder`	`Preorder.toLT` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma`	—	`AddLECancellable.tsub_lt_iff_right` `Contravariant.AddLECancellable`
`tsub_lt_iff_tsub_lt` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder`	`Preorder.toLT`	—	`AddLECancellable.tsub_lt_iff_tsub_lt` `Contravariant.AddLECancellable`
`tsub_lt_tsub_iff_left_of_le_of_le` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder`	`Preorder.toLT`	—	`AddLECancellable.tsub_lt_tsub_iff_left_of_le_of_le` `Contravariant.AddLECancellable`
`tsub_lt_tsub_left_of_le` 📖	—	`Preorder.toLE` `PartialOrder.toPreorder` `Preorder.toLT`	—	—	`AddLECancellable.tsub_lt_tsub_left_of_le` `Contravariant.AddLECancellable`
`tsub_lt_tsub_right_of_le` 📖	—	`Preorder.toLE` `PartialOrder.toPreorder` `Preorder.toLT`	—	—	`AddLECancellable.tsub_lt_tsub_right_of_le` `Contravariant.AddLECancellable`
`tsub_tsub_assoc` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder`	`AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma`	—	`AddLECancellable.tsub_tsub_assoc` `Contravariant.AddLECancellable`
`tsub_tsub_cancel_of_le` 📖	—	`Preorder.toLE` `PartialOrder.toPreorder`	—	—	`AddLECancellable.tsub_tsub_cancel_of_le` `Contravariant.AddLECancellable`
`tsub_tsub_eq_add_tsub_of_le` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder`	`AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma`	—	`ExistsAddOfLE.exists_add_of_le` `add_tsub_cancel_left` `add_comm` `add_tsub_add_eq_tsub_left`
`tsub_tsub_tsub_cancel_left` 📖	—	`Preorder.toLE` `PartialOrder.toPreorder`	—	—	`AddLECancellable.tsub_tsub_tsub_cancel_left` `Contravariant.AddLECancellable`
`tsub_tsub_tsub_cancel_right` 📖	—	`Preorder.toLE` `PartialOrder.toPreorder`	—	—	`tsub_tsub` `add_tsub_cancel_of_le`

---

← Back to Index