Basic

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

Statistics

Metric	Count
Definitions `toSub`, `toAddCancelCommMonoid`	2
Theorems `lt_tsub_iff_left`, `lt_tsub_iff_right`, `tsub_le_tsub_iff_left`, `tsub_lt_self`, `tsub_lt_self_iff`, `tsub_lt_tsub_iff_left_of_le`, `tsub_lt_tsub_iff_right`, `tsub_right_inj`, `toOrderedSub`, `tsub`, `add_tsub_cancel_iff_le`, `add_tsub_eq_max`, `tsub_add_cancel_iff_le`, `tsub_add_eq_max`, `tsub_add_min`, `tsub_eq_tsub_min`, `tsub_eq_zero_iff_le`, `tsub_eq_zero_of_le`, `tsub_le_self`, `tsub_le_tsub_iff_left`, `tsub_lt_of_lt`, `tsub_lt_self`, `tsub_lt_self_iff`, `tsub_lt_tsub_iff_left_of_le`, `tsub_lt_tsub_iff_right`, `tsub_min`, `tsub_pos_iff_lt`, `tsub_pos_iff_not_le`, `tsub_pos_of_lt`, `tsub_right_inj`, `tsub_self`, `tsub_self_add`, `tsub_tsub_eq_min`, `zero_tsub`	34
Total	36

AddLECancellable

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`lt_tsub_iff_left` 📖	mathematical	`AddLECancellable` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`Preorder.toLT`	—	`lt_imp_lt_of_le_imp_le` `tsub_le_iff_left` `lt_tsub_of_add_lt_left`
`lt_tsub_iff_right` 📖	mathematical	`AddLECancellable` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`Preorder.toLT`	—	`lt_imp_lt_of_le_imp_le` `tsub_le_iff_right` `lt_tsub_of_add_lt_right`
`tsub_le_tsub_iff_left` 📖	—	`AddLECancellable` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `Preorder.toLE` `PartialOrder.toPreorder`	—	—	`tsub_le_iff_left` `add_tsub_assoc_of_le` `CanonicallyOrderedAdd.toExistsAddOfLE` `CanonicallyOrderedAdd.toAddLeftMono` `le_tsub_iff_right` `LE.le.trans` `le_add_self` `add_comm` `tsub_le_tsub_left`
`tsub_lt_self` 📖	—	`AddLECancellable` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Preorder.toLT` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid`	—	—	`LE.le.lt_of_ne` `tsub_le_self` `LT.lt.not_ge` `add_le_iff_nonpos_left` `AddCommMagma.to_isCommutative` `CanonicallyOrderedAdd.toAddLeftMono` `add_le_of_le_tsub_left_of_le` `CanonicallyOrderedAdd.toExistsAddOfLE` `LT.lt.le` `tsub_pos_iff_lt` `Eq.ge`
`tsub_lt_self_iff` 📖	mathematical	`AddLECancellable` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`Preorder.toLT` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid`	—	`LE.le.trans_lt` `zero_le` `LE.le.lt_of_ne` `LT.lt.false` `tsub_zero` `tsub_lt_self`
`tsub_lt_tsub_iff_left_of_le` 📖	mathematical	`AddLECancellable` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`Preorder.toLT`	—	`lt_iff_lt_of_le_iff_le` `tsub_le_tsub_iff_left`
`tsub_lt_tsub_iff_right` 📖	mathematical	`AddLECancellable` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`Preorder.toLT`	—	`lt_tsub_iff_left` `add_tsub_cancel_of_le` `CanonicallyOrderedAdd.toExistsAddOfLE` `CanonicallyOrderedAdd.toAddLeftMono`
`tsub_right_inj` 📖	—	`AddLECancellable` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `Preorder.toLE` `PartialOrder.toPreorder`	—	—	`tsub_le_tsub_iff_left`

CanonicallyOrderedAdd

Definitions

Name	Category	Theorems
`toSub` 📖	CompOp	1 math math: `toOrderedSub`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`toOrderedSub` 📖	mathematical	—	`OrderedSub` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `toSub`	—	`ExistsAddOfLE.exists_add_of_le` `toExistsAddOfLE` `add_comm` `add_le_add_iff_right` `covariant_swap_add_of_covariant_add` `toAddLeftMono` `zero_add` `add_le_add` `LT.lt.le` `not_le` `zero_le`

CanonicallyOrderedAddCommMonoid

Definitions

Name	Category	Theorems
`toAddCancelCommMonoid` 📖	CompOp	—

Even

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`tsub` 📖	—	`Even` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup`	—	—	`le_total` `tsub_eq_zero_of_le` `add_le_add` `CanonicallyOrderedAdd.toAddLeftMono` `covariant_swap_add_of_covariant_add` `add_zero` `tsub_add_tsub_comm` `CanonicallyOrderedAdd.toExistsAddOfLE`

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`add_tsub_cancel_iff_le` 📖	mathematical	—	`AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `Preorder.toLE` `PartialOrder.toPreorder`	—	`le_iff_exists_add` `add_tsub_cancel_of_le` `CanonicallyOrderedAdd.toExistsAddOfLE` `CanonicallyOrderedAdd.toAddLeftMono`
`add_tsub_eq_max` 📖	mathematical	—	`AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	—	`add_comm` `max_comm` `tsub_add_eq_max`
`tsub_add_cancel_iff_le` 📖	mathematical	—	`AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `Preorder.toLE` `PartialOrder.toPreorder`	—	`add_comm` `add_tsub_cancel_iff_le`
`tsub_add_eq_max` 📖	mathematical	—	`AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	—	`le_total` `max_eq_right` `tsub_eq_zero_of_le` `zero_add` `max_eq_left` `tsub_add_cancel_of_le` `CanonicallyOrderedAdd.toExistsAddOfLE` `CanonicallyOrderedAdd.toAddLeftMono`
`tsub_add_min` 📖	mathematical	—	`AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `SemilatticeInf.toMin` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	—	`tsub_min` `tsub_add_cancel_of_le` `CanonicallyOrderedAdd.toExistsAddOfLE` `CanonicallyOrderedAdd.toAddLeftMono` `min_le_left`
`tsub_eq_tsub_min` 📖	mathematical	—	`SemilatticeInf.toMin` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	—	`le_total` `min_eq_left` `tsub_self` `tsub_eq_zero_of_le` `min_eq_right`
`tsub_eq_zero_iff_le` 📖	mathematical	—	`AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `Preorder.toLE` `PartialOrder.toPreorder`	—	`nonpos_iff_eq_zero` `tsub_le_iff_left` `add_zero`
`tsub_eq_zero_of_le` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder`	`AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid`	—	`tsub_eq_zero_iff_le`
`tsub_le_self` 📖	mathematical	—	`Preorder.toLE` `PartialOrder.toPreorder`	—	`tsub_le_iff_left` `le_add_left` `le_rfl`
`tsub_le_tsub_iff_left` 📖	—	`Preorder.toLE` `PartialOrder.toPreorder`	—	—	`AddLECancellable.tsub_le_tsub_iff_left` `Contravariant.AddLECancellable`
`tsub_lt_of_lt` 📖	—	`Preorder.toLT` `PartialOrder.toPreorder`	—	—	`lt_of_le_of_lt` `tsub_le_self`
`tsub_lt_self` 📖	—	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid`	—	—	`AddLECancellable.tsub_lt_self` `Contravariant.AddLECancellable`
`tsub_lt_self_iff` 📖	mathematical	—	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid`	—	`AddLECancellable.tsub_lt_self_iff` `Contravariant.AddLECancellable`
`tsub_lt_tsub_iff_left_of_le` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`Preorder.toLT`	—	`AddLECancellable.tsub_lt_tsub_iff_left_of_le` `Contravariant.AddLECancellable`
`tsub_lt_tsub_iff_right` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`Preorder.toLT`	—	`AddLECancellable.tsub_lt_tsub_iff_right` `Contravariant.AddLECancellable`
`tsub_min` 📖	mathematical	—	`SemilatticeInf.toMin` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	—	`tsub_eq_tsub_min`
`tsub_pos_iff_lt` 📖	mathematical	—	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid`	—	`tsub_pos_iff_not_le` `not_le`
`tsub_pos_iff_not_le` 📖	mathematical	—	`Preorder.toLT` `PartialOrder.toPreorder` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `Preorder.toLE`	—	`pos_iff_ne_zero` `tsub_eq_zero_iff_le`
`tsub_pos_of_lt` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder`	`AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid`	—	`tsub_pos_iff_not_le` `LT.lt.not_ge`
`tsub_right_inj` 📖	—	`Preorder.toLE` `PartialOrder.toPreorder`	—	—	`Contravariant.AddLECancellable`
`tsub_self` 📖	mathematical	—	`AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid`	—	`tsub_eq_zero_of_le` `le_rfl`
`tsub_self_add` 📖	mathematical	—	`AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid`	—	`tsub_eq_zero_of_le` `self_le_add_right`
`tsub_tsub_eq_min` 📖	mathematical	—	`SemilatticeInf.toMin` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	—	`tsub_eq_tsub_min` `tsub_tsub_cancel_of_le` `CanonicallyOrderedAdd.toExistsAddOfLE` `CanonicallyOrderedAdd.toAddLeftMono` `min_le_left`
`zero_tsub` 📖	mathematical	—	`AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid`	—	`tsub_eq_zero_of_le` `zero_le`

---

← Back to Index