Hom

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

Statistics

Metric	Count
Definitions	0
Theorems le_map_tsub, le_map_tsub, map_tsub, le_mul_tsub, le_tsub_mul, map_tsub_of_le	6
Total	6

AddHom

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
le_map_tsub 📖	mathematical	Monotone DFunLike.coe AddHom funLike	Preorder.toLE DFunLike.coe AddHom funLike	—	tsub_le_iff_right map_add le_tsub_add

AddMonoidHom

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
le_map_tsub 📖	mathematical	Monotone DFunLike.coe AddMonoidHom AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid instFunLike	Preorder.toLE DFunLike.coe AddMonoidHom AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid instFunLike	—	AddHom.le_map_tsub

OrderIso

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
map_tsub 📖	mathematical	DFunLike.coe OrderIso Preorder.toLE PartialOrder.toPreorder instFunLikeOrderIso	DFunLike.coe OrderIso Preorder.toLE PartialOrder.toPreorder instFunLikeOrderIso	—	le_antisymm monotone AddHom.le_map_tsub symm_apply_apply apply_symm_apply

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
le_mul_tsub 📖	mathematical	—	Preorder.toLE Distrib.toMul	—	AddHom.le_map_tsub Monotone.const_mul' monotone_id
le_tsub_mul 📖	mathematical	—	Preorder.toLE Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalSemiring.toNonUnitalNonAssocSemiring NonUnitalCommSemiring.toNonUnitalSemiring	—	mul_comm le_mul_tsub
map_tsub_of_le 📖	mathematical	Preorder.toLE PartialOrder.toPreorder	DFunLike.coe	—	tsub_add_cancel_of_le map_add add_tsub_cancel_right

---

← Back to Index