Monoid

📁 Source: Mathlib/Algebra/Order/Interval/Set/Monoid.lean

Statistics

Metric	Count
Definitions	0
Theorems Icc_add_bij, Ici_add_bij, Ico_add_bij, Ioc_add_bij, Ioi_add_bij, Ioo_add_bij, image_add_const_Icc, image_add_const_Ici, image_add_const_Ico, image_add_const_Ioc, image_add_const_Ioi, image_add_const_Ioo, image_const_add_Icc, image_const_add_Ici, image_const_add_Ico, image_const_add_Ioc, image_const_add_Ioi, image_const_add_Ioo	18
Total	18

Set

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
Icc_add_bij 📖	mathematical	—	BijOn AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup Icc PartialOrder.toPreorder	—	Ici_inter_Iic BijOn.inter_mapsTo Ici_add_bij covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono IsOrderedCancelAddMonoid.toIsOrderedAddMonoid IsRightCancelAdd.addRightReflectLE_of_addRightReflectLT IsCancelAdd.toIsRightCancelAdd IsOrderedCancelAddMonoid.toIsCancelAdd contravariant_swap_add_of_contravariant_add IsOrderedCancelAddMonoid.toAddLeftReflectLT le_of_add_le_add_right
Ici_add_bij 📖	mathematical	—	BijOn AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup Ici PartialOrder.toPreorder	—	covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono IsOrderedCancelAddMonoid.toIsOrderedAddMonoid IsRightCancelAdd.addRightReflectLE_of_addRightReflectLT IsCancelAdd.toIsRightCancelAdd IsOrderedCancelAddMonoid.toIsCancelAdd contravariant_swap_add_of_contravariant_add IsOrderedCancelAddMonoid.toAddLeftReflectLT ExistsAddOfLE.exists_add_of_le mem_Ici add_le_add_iff_right add_right_comm
Ico_add_bij 📖	mathematical	—	BijOn AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup Ico PartialOrder.toPreorder	—	Ici_inter_Iio BijOn.inter_mapsTo Ici_add_bij IsRightCancelAdd.addRightStrictMono_of_addRightMono IsCancelAdd.toIsRightCancelAdd IsOrderedCancelAddMonoid.toIsCancelAdd covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono IsOrderedCancelAddMonoid.toIsOrderedAddMonoid contravariant_swap_add_of_contravariant_add IsOrderedCancelAddMonoid.toAddLeftReflectLT lt_of_add_lt_add_right
Ioc_add_bij 📖	mathematical	—	BijOn AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup Ioc PartialOrder.toPreorder	—	Ioi_inter_Iic BijOn.inter_mapsTo Ioi_add_bij covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono IsOrderedCancelAddMonoid.toIsOrderedAddMonoid IsRightCancelAdd.addRightReflectLE_of_addRightReflectLT IsCancelAdd.toIsRightCancelAdd IsOrderedCancelAddMonoid.toIsCancelAdd contravariant_swap_add_of_contravariant_add IsOrderedCancelAddMonoid.toAddLeftReflectLT le_of_add_le_add_right
Ioi_add_bij 📖	mathematical	—	BijOn AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup Ioi PartialOrder.toPreorder	—	IsRightCancelAdd.addRightStrictMono_of_addRightMono IsCancelAdd.toIsRightCancelAdd IsOrderedCancelAddMonoid.toIsCancelAdd covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono IsOrderedCancelAddMonoid.toIsOrderedAddMonoid contravariant_swap_add_of_contravariant_add IsOrderedCancelAddMonoid.toAddLeftReflectLT ExistsAddOfLE.exists_add_of_le LT.lt.le mem_Ioi add_lt_add_iff_right add_right_comm
Ioo_add_bij 📖	mathematical	—	BijOn AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup Ioo PartialOrder.toPreorder	—	Ioi_inter_Iio BijOn.inter_mapsTo Ioi_add_bij IsRightCancelAdd.addRightStrictMono_of_addRightMono IsCancelAdd.toIsRightCancelAdd IsOrderedCancelAddMonoid.toIsCancelAdd covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono IsOrderedCancelAddMonoid.toIsOrderedAddMonoid contravariant_swap_add_of_contravariant_add IsOrderedCancelAddMonoid.toAddLeftReflectLT lt_of_add_lt_add_right
image_add_const_Icc 📖	mathematical	—	image AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup Icc PartialOrder.toPreorder	—	BijOn.image_eq Icc_add_bij
image_add_const_Ici 📖	mathematical	—	image AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup Ici PartialOrder.toPreorder	—	BijOn.image_eq Ici_add_bij
image_add_const_Ico 📖	mathematical	—	image AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup Ico PartialOrder.toPreorder	—	BijOn.image_eq Ico_add_bij
image_add_const_Ioc 📖	mathematical	—	image AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup Ioc PartialOrder.toPreorder	—	BijOn.image_eq Ioc_add_bij
image_add_const_Ioi 📖	mathematical	—	image AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup Ioi PartialOrder.toPreorder	—	BijOn.image_eq Ioi_add_bij
image_add_const_Ioo 📖	mathematical	—	image AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup Ioo PartialOrder.toPreorder	—	BijOn.image_eq Ioo_add_bij
image_const_add_Icc 📖	mathematical	—	image AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup Icc PartialOrder.toPreorder	—	image_congr add_comm image_add_const_Icc
image_const_add_Ici 📖	mathematical	—	image AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup Ici PartialOrder.toPreorder	—	image_congr add_comm image_add_const_Ici
image_const_add_Ico 📖	mathematical	—	image AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup Ico PartialOrder.toPreorder	—	image_congr add_comm image_add_const_Ico
image_const_add_Ioc 📖	mathematical	—	image AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup Ioc PartialOrder.toPreorder	—	image_congr add_comm image_add_const_Ioc
image_const_add_Ioi 📖	mathematical	—	image AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup Ioi PartialOrder.toPreorder	—	image_congr add_comm image_add_const_Ioi
image_const_add_Ioo 📖	mathematical	—	image AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup Ioo PartialOrder.toPreorder	—	image_congr add_comm image_add_const_Ioo

---

← Back to Index