Multiset

📁 Source: Mathlib/Algebra/Order/Interval/Multiset.lean

Statistics

Metric	Count
Definitions	0
Theorems 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	8
Total	8

Multiset

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
map_add_left_Icc 📖	mathematical	—	map AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup Icc PartialOrder.toPreorder	—	Icc.eq_1 Finset.image_add_left_Icc Finset.image_val Nodup.dedup Nodup.map add_right_injective IsCancelAdd.toIsLeftCancelAdd IsOrderedCancelAddMonoid.toIsCancelAdd Finset.nodup
map_add_left_Ico 📖	mathematical	—	map AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup Ico PartialOrder.toPreorder	—	Ico.eq_1 Finset.image_add_left_Ico Finset.image_val Nodup.dedup Nodup.map add_right_injective IsCancelAdd.toIsLeftCancelAdd IsOrderedCancelAddMonoid.toIsCancelAdd Finset.nodup
map_add_left_Ioc 📖	mathematical	—	map AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup Ioc PartialOrder.toPreorder	—	Ioc.eq_1 Finset.image_add_left_Ioc Finset.image_val Nodup.dedup Nodup.map add_right_injective IsCancelAdd.toIsLeftCancelAdd IsOrderedCancelAddMonoid.toIsCancelAdd Finset.nodup
map_add_left_Ioo 📖	mathematical	—	map AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup Ioo PartialOrder.toPreorder	—	Ioo.eq_1 Finset.image_add_left_Ioo Finset.image_val Nodup.dedup Nodup.map add_right_injective IsCancelAdd.toIsLeftCancelAdd IsOrderedCancelAddMonoid.toIsCancelAdd Finset.nodup
map_add_right_Icc 📖	mathematical	—	map AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup Icc PartialOrder.toPreorder	—	map_congr add_comm map_add_left_Icc
map_add_right_Ico 📖	mathematical	—	map AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup Ico PartialOrder.toPreorder	—	map_congr add_comm map_add_left_Ico
map_add_right_Ioc 📖	mathematical	—	map AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup Ioc PartialOrder.toPreorder	—	map_congr add_comm map_add_left_Ioc
map_add_right_Ioo 📖	mathematical	—	map AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup Ioo PartialOrder.toPreorder	—	map_congr add_comm map_add_left_Ioo

---

← Back to Index