Basic

📁 Source: Mathlib/Algebra/Order/Interval/Finset/Basic.lean

Statistics

Metric	Count
Definitions	0
Theorems image_add_left_Icc, image_add_left_Ico, image_add_left_Ioc, image_add_left_Ioo, image_add_right_Icc, image_add_right_Ico, image_add_right_Ioc, image_add_right_Ioo, map_add_left_Icc, map_add_left_Ico, map_add_left_Ioc, map_add_left_Ioo, map_add_right_Icc, map_add_right_Ico, map_add_right_Ioc, map_add_right_Ioo	16
Total	16

Finset

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
image_add_left_Icc 📖	mathematical	—	image AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup Icc PartialOrder.toPreorder	—	IsCancelAdd.toIsLeftCancelAdd IsOrderedCancelAddMonoid.toIsCancelAdd map_add_left_Icc map_eq_image add_right_injective addLeftEmbedding.eq_1
image_add_left_Ico 📖	mathematical	—	image AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup Ico PartialOrder.toPreorder	—	IsCancelAdd.toIsLeftCancelAdd IsOrderedCancelAddMonoid.toIsCancelAdd map_add_left_Ico map_eq_image add_right_injective addLeftEmbedding.eq_1
image_add_left_Ioc 📖	mathematical	—	image AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup Ioc PartialOrder.toPreorder	—	IsCancelAdd.toIsLeftCancelAdd IsOrderedCancelAddMonoid.toIsCancelAdd map_add_left_Ioc map_eq_image add_right_injective addLeftEmbedding.eq_1
image_add_left_Ioo 📖	mathematical	—	image AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup Ioo PartialOrder.toPreorder	—	IsCancelAdd.toIsLeftCancelAdd IsOrderedCancelAddMonoid.toIsCancelAdd map_add_left_Ioo map_eq_image add_right_injective addLeftEmbedding.eq_1
image_add_right_Icc 📖	mathematical	—	image AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup Icc PartialOrder.toPreorder	—	IsCancelAdd.toIsRightCancelAdd IsOrderedCancelAddMonoid.toIsCancelAdd map_add_right_Icc map_eq_image add_left_injective addRightEmbedding.eq_1
image_add_right_Ico 📖	mathematical	—	image AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup Ico PartialOrder.toPreorder	—	IsCancelAdd.toIsRightCancelAdd IsOrderedCancelAddMonoid.toIsCancelAdd map_add_right_Ico map_eq_image add_left_injective addRightEmbedding.eq_1
image_add_right_Ioc 📖	mathematical	—	image AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup Ioc PartialOrder.toPreorder	—	IsCancelAdd.toIsRightCancelAdd IsOrderedCancelAddMonoid.toIsCancelAdd map_add_right_Ioc map_eq_image add_left_injective addRightEmbedding.eq_1
image_add_right_Ioo 📖	mathematical	—	image AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup Ioo PartialOrder.toPreorder	—	IsCancelAdd.toIsRightCancelAdd IsOrderedCancelAddMonoid.toIsCancelAdd map_add_right_Ioo map_eq_image add_left_injective addRightEmbedding.eq_1
map_add_left_Icc 📖	mathematical	—	map addLeftEmbedding AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup IsCancelAdd.toIsLeftCancelAdd IsOrderedCancelAddMonoid.toIsCancelAdd Icc PartialOrder.toPreorder	—	IsCancelAdd.toIsLeftCancelAdd IsOrderedCancelAddMonoid.toIsCancelAdd coe_map coe_Icc Set.image_const_add_Icc
map_add_left_Ico 📖	mathematical	—	map addLeftEmbedding AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup IsCancelAdd.toIsLeftCancelAdd IsOrderedCancelAddMonoid.toIsCancelAdd Ico PartialOrder.toPreorder	—	IsCancelAdd.toIsLeftCancelAdd IsOrderedCancelAddMonoid.toIsCancelAdd coe_map coe_Ico Set.image_const_add_Ico
map_add_left_Ioc 📖	mathematical	—	map addLeftEmbedding AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup IsCancelAdd.toIsLeftCancelAdd IsOrderedCancelAddMonoid.toIsCancelAdd Ioc PartialOrder.toPreorder	—	IsCancelAdd.toIsLeftCancelAdd IsOrderedCancelAddMonoid.toIsCancelAdd coe_map coe_Ioc Set.image_const_add_Ioc
map_add_left_Ioo 📖	mathematical	—	map addLeftEmbedding AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup IsCancelAdd.toIsLeftCancelAdd IsOrderedCancelAddMonoid.toIsCancelAdd Ioo PartialOrder.toPreorder	—	IsCancelAdd.toIsLeftCancelAdd IsOrderedCancelAddMonoid.toIsCancelAdd coe_map coe_Ioo Set.image_const_add_Ioo
map_add_right_Icc 📖	mathematical	—	map addRightEmbedding AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup IsCancelAdd.toIsRightCancelAdd IsOrderedCancelAddMonoid.toIsCancelAdd Icc PartialOrder.toPreorder	—	IsCancelAdd.toIsRightCancelAdd IsOrderedCancelAddMonoid.toIsCancelAdd coe_map coe_Icc Set.image_add_const_Icc
map_add_right_Ico 📖	mathematical	—	map addRightEmbedding AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup IsCancelAdd.toIsRightCancelAdd IsOrderedCancelAddMonoid.toIsCancelAdd Ico PartialOrder.toPreorder	—	IsCancelAdd.toIsRightCancelAdd IsOrderedCancelAddMonoid.toIsCancelAdd coe_map coe_Ico Set.image_add_const_Ico
map_add_right_Ioc 📖	mathematical	—	map addRightEmbedding AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup IsCancelAdd.toIsRightCancelAdd IsOrderedCancelAddMonoid.toIsCancelAdd Ioc PartialOrder.toPreorder	—	IsCancelAdd.toIsRightCancelAdd IsOrderedCancelAddMonoid.toIsCancelAdd coe_map coe_Ioc Set.image_add_const_Ioc
map_add_right_Ioo 📖	mathematical	—	map addRightEmbedding AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup IsCancelAdd.toIsRightCancelAdd IsOrderedCancelAddMonoid.toIsCancelAdd Ioo PartialOrder.toPreorder	—	IsCancelAdd.toIsRightCancelAdd IsOrderedCancelAddMonoid.toIsCancelAdd coe_map coe_Ioo Set.image_add_const_Ioo

---

← Back to Index