Defs

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

Statistics

Metric	Count
Definitions `OrderedSub`	1
Theorems `add_tsub_cancel_left`, `add_tsub_cancel_right`, `eq_tsub_of_add_eq`, `eq_tsub_of_add_eq'`, `le_add_tsub`, `le_add_tsub_swap`, `le_tsub_of_add_le_left`, `le_tsub_of_add_le_right`, `lt_add_of_tsub_lt_left`, `lt_add_of_tsub_lt_right`, `lt_tsub_of_add_lt_left`, `lt_tsub_of_add_lt_right`, `tsub_eq_of_eq_add`, `tsub_eq_of_eq_add'`, `tsub_eq_of_eq_add_rev`, `tsub_eq_of_eq_add_rev'`, `tsub_le_iff_right`, `add_le_add_add_tsub`, `add_tsub_add_eq_tsub_left`, `add_tsub_add_eq_tsub_right`, `add_tsub_add_le_tsub_add_tsub`, `add_tsub_add_le_tsub_left`, `add_tsub_add_le_tsub_right`, `add_tsub_cancel_left`, `add_tsub_cancel_right`, `add_tsub_le_assoc`, `add_tsub_le_left`, `add_tsub_le_right`, `add_tsub_le_tsub_add`, `antitone_const_tsub`, `eq_tsub_of_add_eq`, `le_add_tsub`, `le_add_tsub'`, `le_add_tsub_swap`, `le_tsub_add`, `le_tsub_add_add`, `le_tsub_of_add_le_left`, `le_tsub_of_add_le_right`, `lt_add_of_tsub_lt_left`, `lt_add_of_tsub_lt_right`, `lt_of_tsub_lt_tsub_left`, `lt_of_tsub_lt_tsub_right`, `lt_tsub_comm`, `lt_tsub_iff_left`, `lt_tsub_iff_right`, `lt_tsub_of_add_lt_left`, `lt_tsub_of_add_lt_right`, `tsub_add_eq_tsub_tsub`, `tsub_add_eq_tsub_tsub_swap`, `tsub_eq_of_eq_add`, `tsub_eq_of_eq_add_rev`, `tsub_eq_tsub_of_add_eq_add`, `tsub_le_iff_left`, `tsub_le_iff_right`, `tsub_le_iff_tsub_le`, `tsub_le_tsub`, `tsub_le_tsub_add_tsub`, `tsub_le_tsub_left`, `tsub_le_tsub_right`, `tsub_nonpos`, `tsub_nonpos_of_le`, `tsub_right_comm`, `tsub_tsub`, `tsub_tsub_le`, `tsub_tsub_le_tsub_add`, `tsub_tsub_tsub_le_tsub`, `tsub_zero`	67
Total	68

AddLECancellable

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`add_tsub_cancel_left` 📖	mathematical	`AddLECancellable` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `Preorder.toLE` `PartialOrder.toPreorder`	`AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma`	—	`tsub_eq_of_eq_add` `add_comm`
`add_tsub_cancel_right` 📖	mathematical	`AddLECancellable` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `Preorder.toLE` `PartialOrder.toPreorder`	`AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma`	—	`tsub_eq_of_eq_add` `add_comm`
`eq_tsub_of_add_eq` 📖	—	`AddLECancellable` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `Preorder.toLE` `PartialOrder.toPreorder`	—	—	`tsub_eq_of_eq_add`
`eq_tsub_of_add_eq'` 📖	—	`AddLECancellable` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `Preorder.toLE` `PartialOrder.toPreorder`	—	—	`tsub_eq_of_eq_add'`
`le_add_tsub` 📖	mathematical	`AddLECancellable` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `Preorder.toLE`	`Preorder.toLE` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma`	—	`add_comm` `le_add_tsub_swap`
`le_add_tsub_swap` 📖	mathematical	`AddLECancellable` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `Preorder.toLE`	`Preorder.toLE` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma`	—	`le_add_tsub`
`le_tsub_of_add_le_left` 📖	mathematical	`AddLECancellable` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `Preorder.toLE`	`Preorder.toLE`	—	`LE.le.trans` `le_add_tsub`
`le_tsub_of_add_le_right` 📖	mathematical	`AddLECancellable` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `Preorder.toLE`	`Preorder.toLE`	—	`le_tsub_of_add_le_left` `add_comm`
`lt_add_of_tsub_lt_left` 📖	mathematical	`AddLECancellable` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `Preorder.toLE` `PartialOrder.toPreorder` `Preorder.toLT`	`Preorder.toLT` `PartialOrder.toPreorder` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma`	—	`lt_iff_le_and_ne` `tsub_le_iff_left` `LT.lt.le` `add_tsub_cancel_left`
`lt_add_of_tsub_lt_right` 📖	mathematical	`AddLECancellable` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `Preorder.toLE` `PartialOrder.toPreorder` `Preorder.toLT`	`Preorder.toLT` `PartialOrder.toPreorder` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma`	—	`lt_iff_le_and_ne` `tsub_le_iff_right` `LT.lt.le` `add_tsub_cancel_right`
`lt_tsub_of_add_lt_left` 📖	mathematical	`AddLECancellable` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `Preorder.toLE` `PartialOrder.toPreorder` `Preorder.toLT`	`Preorder.toLT` `PartialOrder.toPreorder`	—	`lt_tsub_of_add_lt_right` `add_comm`
`lt_tsub_of_add_lt_right` 📖	mathematical	`AddLECancellable` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `Preorder.toLE` `PartialOrder.toPreorder` `Preorder.toLT`	`Preorder.toLT` `PartialOrder.toPreorder`	—	`LE.le.lt_of_ne` `le_tsub_of_add_le_right` `LT.lt.le` `LT.lt.not_ge` `le_tsub_add`
`tsub_eq_of_eq_add` 📖	—	`AddLECancellable` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `Preorder.toLE` `PartialOrder.toPreorder`	—	—	`le_antisymm` `tsub_le_iff_right` `Eq.le` `le_add_tsub`
`tsub_eq_of_eq_add'` 📖	—	`AddLECancellable` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `Preorder.toLE` `PartialOrder.toPreorder`	—	—	`tsub_eq_of_eq_add` `of_add_right`
`tsub_eq_of_eq_add_rev` 📖	—	`AddLECancellable` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `Preorder.toLE` `PartialOrder.toPreorder`	—	—	`tsub_eq_of_eq_add` `add_comm`
`tsub_eq_of_eq_add_rev'` 📖	—	`AddLECancellable` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `Preorder.toLE` `PartialOrder.toPreorder`	—	—	`tsub_eq_of_eq_add'` `add_comm`

OrderedSub

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`tsub_le_iff_right` 📖	—	—	—	—	—

(root)

Definitions

Name	Category	Theorems
`OrderedSub` 📖	CompData	13 math math: `Nat.instOrderedSub`, `ENNReal.instOrderedSub`, `CanonicallyOrderedAdd.toOrderedSub`, `WithTop.instOrderedSub`, `Prod.orderedSub`, `AddGroup.toOrderedSub`, `Language.instOrderedSub`, `DFinsupp.instOrderedSub`, `NNRat.instOrderedSub`, `Pi.orderedSub`, `Multiset.instOrderedSub`, `Finsupp.orderedSub`, `Nonneg.orderedSub`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`add_le_add_add_tsub` 📖	mathematical	—	`Preorder.toLE` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma`	—	`add_assoc` `le_imp_le_of_le_of_le` `le_refl` `add_le_add_right` `le_add_tsub`
`add_tsub_add_eq_tsub_left` 📖	mathematical	—	`AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma`	—	`add_comm` `add_tsub_add_eq_tsub_right`
`add_tsub_add_eq_tsub_right` 📖	mathematical	—	`AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma`	—	`LE.le.antisymm` `add_tsub_add_le_tsub_right` `tsub_le_iff_right` `le_of_add_le_add_right` `contravariant_swap_add_of_contravariant_add` `add_assoc` `le_tsub_add`
`add_tsub_add_le_tsub_add_tsub` 📖	mathematical	—	`Preorder.toLE` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma`	—	`add_comm` `tsub_le_iff_left` `add_assoc` `LE.le.trans` `tsub_le_tsub_right` `add_tsub_le_assoc`
`add_tsub_add_le_tsub_left` 📖	mathematical	—	`Preorder.toLE` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma`	—	`tsub_le_iff_left` `add_assoc` `le_imp_le_of_le_of_le` `le_refl` `add_le_add_right` `le_add_tsub`
`add_tsub_add_le_tsub_right` 📖	mathematical	—	`Preorder.toLE` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma`	—	`tsub_le_iff_left` `add_right_comm` `le_imp_le_of_le_of_le` `le_refl` `add_le_add_left` `covariant_swap_add_of_covariant_add` `le_add_tsub`
`add_tsub_cancel_left` 📖	mathematical	—	`AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma`	—	`AddLECancellable.add_tsub_cancel_left` `Contravariant.AddLECancellable`
`add_tsub_cancel_right` 📖	mathematical	—	`AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma`	—	`AddLECancellable.add_tsub_cancel_right` `Contravariant.AddLECancellable`
`add_tsub_le_assoc` 📖	mathematical	—	`Preorder.toLE` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma`	—	`tsub_le_iff_left` `add_left_comm` `le_imp_le_of_le_of_le` `le_refl` `add_le_add_right` `le_add_tsub`
`add_tsub_le_left` 📖	mathematical	—	`Preorder.toLE` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma`	—	`tsub_le_iff_left` `le_rfl`
`add_tsub_le_right` 📖	mathematical	—	`Preorder.toLE`	—	`tsub_le_iff_right` `le_rfl`
`add_tsub_le_tsub_add` 📖	mathematical	—	`Preorder.toLE` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma`	—	`add_comm` `add_tsub_le_assoc`
`antitone_const_tsub` 📖	mathematical	—	`Antitone`	—	`tsub_le_tsub` `Eq.le`
`eq_tsub_of_add_eq` 📖	—	`AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma`	—	—	`AddLECancellable.eq_tsub_of_add_eq` `Contravariant.AddLECancellable`
`le_add_tsub` 📖	mathematical	—	`Preorder.toLE` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma`	—	`tsub_le_iff_left` `le_rfl`
`le_add_tsub'` 📖	mathematical	—	`Preorder.toLE` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma`	—	`AddLECancellable.le_add_tsub` `Contravariant.AddLECancellable`
`le_add_tsub_swap` 📖	mathematical	—	`Preorder.toLE` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma`	—	`AddLECancellable.le_add_tsub_swap` `Contravariant.AddLECancellable`
`le_tsub_add` 📖	mathematical	—	`Preorder.toLE`	—	`tsub_le_iff_right` `le_rfl`
`le_tsub_add_add` 📖	mathematical	—	`Preorder.toLE` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma`	—	`add_comm` `add_le_add_add_tsub`
`le_tsub_of_add_le_left` 📖	mathematical	`Preorder.toLE` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma`	`Preorder.toLE`	—	`AddLECancellable.le_tsub_of_add_le_left` `Contravariant.AddLECancellable`
`le_tsub_of_add_le_right` 📖	mathematical	`Preorder.toLE` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma`	`Preorder.toLE`	—	`AddLECancellable.le_tsub_of_add_le_right` `Contravariant.AddLECancellable`
`lt_add_of_tsub_lt_left` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder`	`Preorder.toLT` `PartialOrder.toPreorder` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma`	—	`AddLECancellable.lt_add_of_tsub_lt_left` `Contravariant.AddLECancellable`
`lt_add_of_tsub_lt_right` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder`	`Preorder.toLT` `PartialOrder.toPreorder` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma`	—	`AddLECancellable.lt_add_of_tsub_lt_right` `Contravariant.AddLECancellable`
`lt_of_tsub_lt_tsub_left` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	—	`lt_imp_lt_of_le_imp_le` `tsub_le_tsub_left`
`lt_of_tsub_lt_tsub_right` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	—	`lt_imp_lt_of_le_imp_le` `tsub_le_tsub_right`
`lt_tsub_comm` 📖	mathematical	—	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	—	`lt_tsub_iff_left` `lt_tsub_iff_right`
`lt_tsub_iff_left` 📖	mathematical	—	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma`	—	`lt_iff_lt_of_le_iff_le` `tsub_le_iff_left`
`lt_tsub_iff_right` 📖	mathematical	—	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma`	—	`lt_iff_lt_of_le_iff_le` `tsub_le_iff_right`
`lt_tsub_of_add_lt_left` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma`	`Preorder.toLT` `PartialOrder.toPreorder`	—	`AddLECancellable.lt_tsub_of_add_lt_left` `Contravariant.AddLECancellable`
`lt_tsub_of_add_lt_right` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma`	`Preorder.toLT` `PartialOrder.toPreorder`	—	`AddLECancellable.lt_tsub_of_add_lt_right` `Contravariant.AddLECancellable`
`tsub_add_eq_tsub_tsub` 📖	mathematical	—	`AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma`	—	`tsub_tsub`
`tsub_add_eq_tsub_tsub_swap` 📖	mathematical	—	`AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma`	—	`add_comm` `tsub_add_eq_tsub_tsub`
`tsub_eq_of_eq_add` 📖	—	`AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma`	—	—	`AddLECancellable.tsub_eq_of_eq_add` `Contravariant.AddLECancellable`
`tsub_eq_of_eq_add_rev` 📖	—	`AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma`	—	—	`AddLECancellable.tsub_eq_of_eq_add_rev` `Contravariant.AddLECancellable`
`tsub_eq_tsub_of_add_eq_add` 📖	—	`AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma`	—	—	`add_tsub_cancel_right` `tsub_right_comm`
`tsub_le_iff_left` 📖	mathematical	—	`Preorder.toLE` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma`	—	`tsub_le_iff_right` `add_comm`
`tsub_le_iff_right` 📖	—	—	—	—	`OrderedSub.tsub_le_iff_right`
`tsub_le_iff_tsub_le` 📖	mathematical	—	`Preorder.toLE`	—	`tsub_le_iff_left` `tsub_le_iff_right`
`tsub_le_tsub` 📖	mathematical	`Preorder.toLE`	`Preorder.toLE`	—	`LE.le.trans` `tsub_le_tsub_right` `tsub_le_tsub_left`
`tsub_le_tsub_add_tsub` 📖	mathematical	—	`Preorder.toLE` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma`	—	`tsub_le_iff_left` `add_assoc` `add_right_comm` `le_imp_le_of_le_of_le` `le_refl` `add_le_add_left` `covariant_swap_add_of_covariant_add` `le_add_tsub`
`tsub_le_tsub_left` 📖	mathematical	`Preorder.toLE`	`Preorder.toLE`	—	`tsub_le_iff_left` `LE.le.trans` `le_add_tsub` `add_le_add_left` `covariant_swap_add_of_covariant_add`
`tsub_le_tsub_right` 📖	mathematical	`Preorder.toLE`	`Preorder.toLE`	—	`tsub_le_iff_left` `LE.le.trans` `le_add_tsub`
`tsub_nonpos` 📖	mathematical	—	`Preorder.toLE` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid`	—	`tsub_le_iff_left` `add_zero`
`tsub_nonpos_of_le` 📖	mathematical	`Preorder.toLE`	`Preorder.toLE` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid`	—	`tsub_nonpos`
`tsub_right_comm` 📖	—	—	—	—	`tsub_add_eq_tsub_tsub` `tsub_add_eq_tsub_tsub_swap`
`tsub_tsub` 📖	mathematical	—	`AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma`	—	`le_antisymm` `tsub_le_iff_left` `add_assoc` `le_refl`
`tsub_tsub_le` 📖	mathematical	—	`Preorder.toLE`	—	`tsub_le_iff_right` `le_add_tsub`
`tsub_tsub_le_tsub_add` 📖	mathematical	—	`Preorder.toLE` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma`	—	`tsub_le_iff_right` `le_tsub_add` `le_imp_le_of_le_of_le` `le_refl` `add_le_add_right` `le_add_tsub` `add_assoc`
`tsub_tsub_tsub_le_tsub` 📖	mathematical	—	`Preorder.toLE`	—	`tsub_le_iff_left` `add_left_comm` `le_imp_le_of_le_of_le` `le_refl` `add_le_add_right` `le_add_tsub` `le_tsub_add`
`tsub_zero` 📖	mathematical	—	`AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid`	—	`AddLECancellable.tsub_eq_of_eq_add` `addLECancellable_zero` `add_zero`

---

← Back to Index