Documentation Verification Report

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`	—	`instIsLeftCancelAddOfAddLeftReflectLE` `IsOrderedCancelAddMonoid.toAddLeftReflectLE` `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`	—	`instIsLeftCancelAddOfAddLeftReflectLE` `IsOrderedCancelAddMonoid.toAddLeftReflectLE` `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`	—	`instIsLeftCancelAddOfAddLeftReflectLE` `IsOrderedCancelAddMonoid.toAddLeftReflectLE` `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`	—	`instIsLeftCancelAddOfAddLeftReflectLE` `IsOrderedCancelAddMonoid.toAddLeftReflectLE` `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`	—	`instIsRightCancelAddOfAddRightReflectLE` `contravariant_swap_add_of_contravariant_add` `IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT` `instIsLeftCancelAddOfAddLeftReflectLE` `IsOrderedCancelAddMonoid.toAddLeftReflectLE` `IsOrderedCancelAddMonoid.toAddLeftReflectLT` `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`	—	`instIsRightCancelAddOfAddRightReflectLE` `contravariant_swap_add_of_contravariant_add` `IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT` `instIsLeftCancelAddOfAddLeftReflectLE` `IsOrderedCancelAddMonoid.toAddLeftReflectLE` `IsOrderedCancelAddMonoid.toAddLeftReflectLT` `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`	—	`instIsRightCancelAddOfAddRightReflectLE` `contravariant_swap_add_of_contravariant_add` `IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT` `instIsLeftCancelAddOfAddLeftReflectLE` `IsOrderedCancelAddMonoid.toAddLeftReflectLE` `IsOrderedCancelAddMonoid.toAddLeftReflectLT` `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`	—	`instIsRightCancelAddOfAddRightReflectLE` `contravariant_swap_add_of_contravariant_add` `IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT` `instIsLeftCancelAddOfAddLeftReflectLE` `IsOrderedCancelAddMonoid.toAddLeftReflectLE` `IsOrderedCancelAddMonoid.toAddLeftReflectLT` `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` `instIsLeftCancelAddOfAddLeftReflectLE` `IsOrderedCancelAddMonoid.toAddLeftReflectLE` `PartialOrder.toPreorder` `Icc`	—	`instIsLeftCancelAddOfAddLeftReflectLE` `IsOrderedCancelAddMonoid.toAddLeftReflectLE` `coe_map` `coe_Icc` `Set.image_const_add_Icc`
`map_add_left_Ico` 📖	mathematical	—	`map` `addLeftEmbedding` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `instIsLeftCancelAddOfAddLeftReflectLE` `IsOrderedCancelAddMonoid.toAddLeftReflectLE` `PartialOrder.toPreorder` `Ico`	—	`instIsLeftCancelAddOfAddLeftReflectLE` `IsOrderedCancelAddMonoid.toAddLeftReflectLE` `coe_map` `coe_Ico` `Set.image_const_add_Ico`
`map_add_left_Ioc` 📖	mathematical	—	`map` `addLeftEmbedding` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `instIsLeftCancelAddOfAddLeftReflectLE` `IsOrderedCancelAddMonoid.toAddLeftReflectLE` `PartialOrder.toPreorder` `Ioc`	—	`instIsLeftCancelAddOfAddLeftReflectLE` `IsOrderedCancelAddMonoid.toAddLeftReflectLE` `coe_map` `coe_Ioc` `Set.image_const_add_Ioc`
`map_add_left_Ioo` 📖	mathematical	—	`map` `addLeftEmbedding` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `instIsLeftCancelAddOfAddLeftReflectLE` `IsOrderedCancelAddMonoid.toAddLeftReflectLE` `PartialOrder.toPreorder` `Ioo`	—	`instIsLeftCancelAddOfAddLeftReflectLE` `IsOrderedCancelAddMonoid.toAddLeftReflectLE` `coe_map` `coe_Ioo` `Set.image_const_add_Ioo`
`map_add_right_Icc` 📖	mathematical	—	`map` `addRightEmbedding` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `instIsRightCancelAddOfAddRightReflectLE` `contravariant_swap_add_of_contravariant_add` `Preorder.toLE` `PartialOrder.toPreorder` `IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT` `instIsLeftCancelAddOfAddLeftReflectLE` `IsOrderedCancelAddMonoid.toAddLeftReflectLE` `IsOrderedCancelAddMonoid.toAddLeftReflectLT` `Icc`	—	`instIsRightCancelAddOfAddRightReflectLE` `contravariant_swap_add_of_contravariant_add` `IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT` `instIsLeftCancelAddOfAddLeftReflectLE` `IsOrderedCancelAddMonoid.toAddLeftReflectLE` `IsOrderedCancelAddMonoid.toAddLeftReflectLT` `coe_map` `coe_Icc` `Set.image_add_const_Icc`
`map_add_right_Ico` 📖	mathematical	—	`map` `addRightEmbedding` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `instIsRightCancelAddOfAddRightReflectLE` `contravariant_swap_add_of_contravariant_add` `Preorder.toLE` `PartialOrder.toPreorder` `IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT` `instIsLeftCancelAddOfAddLeftReflectLE` `IsOrderedCancelAddMonoid.toAddLeftReflectLE` `IsOrderedCancelAddMonoid.toAddLeftReflectLT` `Ico`	—	`instIsRightCancelAddOfAddRightReflectLE` `contravariant_swap_add_of_contravariant_add` `IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT` `instIsLeftCancelAddOfAddLeftReflectLE` `IsOrderedCancelAddMonoid.toAddLeftReflectLE` `IsOrderedCancelAddMonoid.toAddLeftReflectLT` `coe_map` `coe_Ico` `Set.image_add_const_Ico`
`map_add_right_Ioc` 📖	mathematical	—	`map` `addRightEmbedding` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `instIsRightCancelAddOfAddRightReflectLE` `contravariant_swap_add_of_contravariant_add` `Preorder.toLE` `PartialOrder.toPreorder` `IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT` `instIsLeftCancelAddOfAddLeftReflectLE` `IsOrderedCancelAddMonoid.toAddLeftReflectLE` `IsOrderedCancelAddMonoid.toAddLeftReflectLT` `Ioc`	—	`instIsRightCancelAddOfAddRightReflectLE` `contravariant_swap_add_of_contravariant_add` `IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT` `instIsLeftCancelAddOfAddLeftReflectLE` `IsOrderedCancelAddMonoid.toAddLeftReflectLE` `IsOrderedCancelAddMonoid.toAddLeftReflectLT` `coe_map` `coe_Ioc` `Set.image_add_const_Ioc`
`map_add_right_Ioo` 📖	mathematical	—	`map` `addRightEmbedding` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `instIsRightCancelAddOfAddRightReflectLE` `contravariant_swap_add_of_contravariant_add` `Preorder.toLE` `PartialOrder.toPreorder` `IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT` `instIsLeftCancelAddOfAddLeftReflectLE` `IsOrderedCancelAddMonoid.toAddLeftReflectLE` `IsOrderedCancelAddMonoid.toAddLeftReflectLT` `Ioo`	—	`instIsRightCancelAddOfAddRightReflectLE` `contravariant_swap_add_of_contravariant_add` `IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT` `instIsLeftCancelAddOfAddLeftReflectLE` `IsOrderedCancelAddMonoid.toAddLeftReflectLE` `IsOrderedCancelAddMonoid.toAddLeftReflectLT` `coe_map` `coe_Ioo` `Set.image_add_const_Ioo`

---

← Back to Index