Interval

📁 Source: Mathlib/Data/Int/Interval.lean

Statistics

Metric	Count
Definitions `instLocallyFiniteOrder`	1
Theorems `Icc_succ_succ`, `Ico_succ_succ`, `Ioc_succ_succ`, `Ioo_succ_succ`, `Icc_eq_finset_map`, `Icc_eq_pair`, `Ico_eq_finset_map`, `Ioc_eq_finset_map`, `Ioo_eq_finset_map`, `card_Icc`, `card_Icc_of_le`, `card_Ico`, `card_Ico_of_le`, `card_Ioc`, `card_Ioc_of_le`, `card_Ioo`, `card_Ioo_of_lt`, `card_fintype_Icc_of_le`, `card_fintype_Ico_of_le`, `card_fintype_Ioc_of_le`, `card_fintype_Ioo_of_lt`, `card_uIcc`, `image_Ico_emod`, `uIcc_eq_finset_map`	24
Total	25

Finset

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`Icc_succ_succ` 📖	mathematical	—	`Icc` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `instLatticeInt` `Int.instLocallyFiniteOrder` `Finset` `instUnion` `instInsert` `instSingleton`	—	`ext` `union_insert` `union_singleton`
`Ico_succ_succ` 📖	mathematical	—	`Ico` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `instLatticeInt` `Int.instLocallyFiniteOrder` `Finset` `instUnion` `instInsert` `instSingleton`	—	`ext` `union_insert` `union_singleton`
`Ioc_succ_succ` 📖	mathematical	—	`Ioc` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `instLatticeInt` `Int.instLocallyFiniteOrder` `Finset` `instUnion` `instInsert` `instSingleton`	—	`ext` `union_insert` `union_singleton`
`Ioo_succ_succ` 📖	mathematical	—	`Ioo` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `instLatticeInt` `Int.instLocallyFiniteOrder` `Finset` `instUnion` `instInsert` `instSingleton`	—	`ext` `union_insert` `union_singleton`

Int

Definitions

Name	Category	Theorems
`instLocallyFiniteOrder` 📖	CompOp	72 math math: `EisensteinSeries.hasSum_e2Summand_symmetricIcc`, `Nat.Ioc_filter_modEq_cast`, `Finset.Icc_succ_succ`, `Finset.prod_Icc_eq_prod_Ico_mul`, `card_Ioo`, `Finset.sum_Ico_le_sum`, `Finset.sum_Ico_int_sub`, `setOf_liouvilleWith_subset_aux`, `LieModule.genWeightSpaceChain_def'`, `IsStrictOrderedRing.int_mem_Icc_of_mul_mem_Ioo`, `EisensteinSeries.tsum_symmetricIco_linear_sub_linear_add_one_eq_zero`, `EisensteinSeries.G2_eq_tsum_symmetricIco`, `card_Ioc`, `SummationFilter.hasSum_symmetricIoc_int_iff`, `card_fintype_Ioo_of_lt`, `card_box`, `Ioo_eq_finset_map`, `Finset.prod_Ico_int_div`, `SummationFilter.hasSum_symmetricIcc_iff`, `card_Ico_of_le`, `FixedDetMatrices.reps_entries_le_m'`, `EisensteinSeries.hasSum_e2Summand_symmetricIco`, `Ioc_filter_modEq_card`, `Finset.sum_Icc_eq_sum_Ico_add`, `card_Ico`, `card_Ioc_of_le`, `Finset.Ioc_succ_succ`, `image_Ico_emod`, `card_fintype_Icc_of_le`, `Icc_eq_finset_map`, `card_fintype_Ioc_of_le`, `Ico_filter_dvd_card`, `Finset.Ico_succ_succ`, `Ioc_eq_finset_map`, `card_uIcc`, `card_Icc_of_le`, `Nat.Ico_filter_modEq_cast`, `SummationFilter.hasProd_symmetricIco_int_iff`, `SummationFilter.hasSum_symmetricIco_int_iff`, `uIcc_eq_finset_map`, `existsUnique_mem_box`, `EisensteinSeries.tsum_tsum_symmetricIco_sub_eq`, `Icc_eq_pair`, `card_Icc`, `EisensteinSeries.tendsto_double_sum_S_act`, `SummationFilter.symmetricIcc_eq_symmetricIoo_int`, `Finset.sum_Icc_of_even_eq_range`, `EisensteinSeries.summable_e2Summand_symmetricIcc`, `Ico_filter_modEq_card`, `Ioc_filter_dvd_eq`, `LieAlgebra.IsKilling.rootSpace_zsmul_add_ne_bot_iff_mem`, `Finset.Ioo_succ_succ`, `mem_box`, `Ico_eq_finset_map`, `Finset.prod_Icc_succ_eq_mul_endpoints`, `EisensteinSeries.tendsto_tsum_one_div_linear_sub_succ_eq`, `card_fintype_Ico_of_le`, `EisensteinSeries.summable_e2Summand_symmetricIco`, `SummationFilter.symmetricIcc_eq_map_Icc_nat`, `Finset.prod_Icc_of_even_eq_range`, `Ico_filter_modEq_eq`, `SummationFilter.hasProd_symmetricIcc_iff`, `Ioc_filter_modEq_eq`, `ZLattice.sum_piFinset_Icc_rpow_le`, `SummationFilter.hasProd_symmetricIoc_int_iff`, `Ico_filter_dvd_eq`, `Finset.sum_Icc_succ_eq_add_endpoints`, `Finset.sum_le_sum_Ioc`, `card_Ioo_of_lt`, `EisensteinSeries.tsum_symmetricIco_tsum_eq_S_act`, `Ioc_filter_dvd_card`, `EisensteinSeries.tsum_symmetricIco_tsum_sub_eq`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`Icc_eq_finset_map` 📖	mathematical	—	`Finset.Icc` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `instLatticeInt` `instLocallyFiniteOrder` `Finset.map` `Function.Embedding.trans` `Nat.castEmbedding` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `instRing` `instCharZero` `addLeftEmbedding` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `AddLeftCancelMonoid.toAddLeftCancelSemigroup` `AddCancelCommMonoid.toAddLeftCancelMonoid` `AddCommGroup.toAddCancelCommMonoid` `instAddCommGroup` `Finset.range`	—	—
`Icc_eq_pair` 📖	mathematical	—	`Finset.Icc` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `instLatticeInt` `instLocallyFiniteOrder` `Finset` `Finset.instInsert` `Finset.instSingleton`	—	`Finset.ext`
`Ico_eq_finset_map` 📖	mathematical	—	`Finset.Ico` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `instLatticeInt` `instLocallyFiniteOrder` `Finset.map` `Function.Embedding.trans` `Nat.castEmbedding` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `instRing` `instCharZero` `addLeftEmbedding` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `AddLeftCancelMonoid.toAddLeftCancelSemigroup` `AddCancelCommMonoid.toAddLeftCancelMonoid` `AddCommGroup.toAddCancelCommMonoid` `instAddCommGroup` `Finset.range`	—	—
`Ioc_eq_finset_map` 📖	mathematical	—	`Finset.Ioc` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `instLatticeInt` `instLocallyFiniteOrder` `Finset.map` `Function.Embedding.trans` `Nat.castEmbedding` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `instRing` `instCharZero` `addLeftEmbedding` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `AddLeftCancelMonoid.toAddLeftCancelSemigroup` `AddCancelCommMonoid.toAddLeftCancelMonoid` `AddCommGroup.toAddCancelCommMonoid` `instAddCommGroup` `Finset.range`	—	—
`Ioo_eq_finset_map` 📖	mathematical	—	`Finset.Ioo` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `instLatticeInt` `instLocallyFiniteOrder` `Finset.map` `Function.Embedding.trans` `Nat.castEmbedding` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `instRing` `instCharZero` `addLeftEmbedding` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `AddLeftCancelMonoid.toAddLeftCancelSemigroup` `AddCancelCommMonoid.toAddLeftCancelMonoid` `AddCommGroup.toAddCancelCommMonoid` `instAddCommGroup` `Finset.range`	—	—
`card_Icc` 📖	mathematical	—	`Finset.card` `Finset.Icc` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `instLatticeInt` `instLocallyFiniteOrder`	—	`instCharZero` `Finset.card_map` `Finset.card_range`
`card_Icc_of_le` 📖	mathematical	—	`Finset.card` `Finset.Icc` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `instLatticeInt` `instLocallyFiniteOrder`	—	`card_Icc`
`card_Ico` 📖	mathematical	—	`Finset.card` `Finset.Ico` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `instLatticeInt` `instLocallyFiniteOrder`	—	`instCharZero` `Finset.card_map` `Finset.card_range`
`card_Ico_of_le` 📖	mathematical	—	`Finset.card` `Finset.Ico` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `instLatticeInt` `instLocallyFiniteOrder`	—	`card_Ico`
`card_Ioc` 📖	mathematical	—	`Finset.card` `Finset.Ioc` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `instLatticeInt` `instLocallyFiniteOrder`	—	`instCharZero` `Finset.card_map` `Finset.card_range`
`card_Ioc_of_le` 📖	mathematical	—	`Finset.card` `Finset.Ioc` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `instLatticeInt` `instLocallyFiniteOrder`	—	`card_Ioc`
`card_Ioo` 📖	mathematical	—	`Finset.card` `Finset.Ioo` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `instLatticeInt` `instLocallyFiniteOrder`	—	`instCharZero` `Finset.card_map` `Finset.card_range`
`card_Ioo_of_lt` 📖	mathematical	—	`Finset.card` `Finset.Ioo` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `instLatticeInt` `instLocallyFiniteOrder`	—	`card_Ioo` `sub_sub`
`card_fintype_Icc_of_le` 📖	mathematical	—	`Fintype.card` `Set.Elem` `Set.Icc` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `instLatticeInt` `Set.instFintypeIcc` `instLocallyFiniteOrder`	—	`Finset.mem_Icc` `Fintype.card_ofFinset` `card_Icc` `sup_of_le_left`
`card_fintype_Ico_of_le` 📖	mathematical	—	`Fintype.card` `Set.Elem` `Set.Ico` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `instLatticeInt` `Set.instFintypeIco` `instLocallyFiniteOrder`	—	`Finset.mem_Ico` `Fintype.card_ofFinset` `card_Ico` `sup_of_le_left`
`card_fintype_Ioc_of_le` 📖	mathematical	—	`Fintype.card` `Set.Elem` `Set.Ioc` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `instLatticeInt` `Set.instFintypeIoc` `instLocallyFiniteOrder`	—	`Finset.mem_Ioc` `Fintype.card_ofFinset` `card_Ioc` `sup_of_le_left`
`card_fintype_Ioo_of_lt` 📖	mathematical	—	`Fintype.card` `Set.Elem` `Set.Ioo` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `instLatticeInt` `Set.instFintypeIoo` `instLocallyFiniteOrder`	—	`Finset.mem_Ioo` `Fintype.card_ofFinset` `card_Ioo` `toNat_pred_coe_of_pos`
`card_uIcc` 📖	mathematical	—	`Finset.card` `Finset.uIcc` `instLatticeInt` `instLocallyFiniteOrder`	—	`instCharZero` `Finset.card_map` `Finset.card_range` `sub_nonneg_of_le` `covariant_swap_add_of_covariant_add` `instAddLeftMono` `min_le_max` `natCast_natAbs` `add_comm` `add_sub_assoc` `max_sub_min_eq_abs`
`image_Ico_emod` 📖	mathematical	—	`Finset.image` `Finset.Ico` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `instLatticeInt` `instLocallyFiniteOrder`	—	`eq_or_lt_of_le` `add_zero` `Finset.Ico_eq_empty_of_le` `Finset.ext` `LT.lt.ne'` `lt_or_ge` `zero_add` `add_le_add_left` `covariant_swap_add_of_covariant_add` `instAddLeftMono` `add_le_add` `LT.lt.le` `add_lt_add_left` `IsRightCancelAdd.addRightStrictMono_of_addRightMono` `AddRightCancelSemigroup.toIsRightCancelAdd` `mul_add` `Distrib.leftDistribClass` `mul_one` `add_assoc` `LE.le.trans` `Eq.le` `add_comm` `add_lt_add_of_lt_of_le` `le_trans` `IsRightCancelAdd.addRightReflectLE_of_addRightReflectLT` `contravariant_swap_add_of_contravariant_add` `contravariant_lt_of_covariant_le` `ne_of_gt`
`uIcc_eq_finset_map` 📖	mathematical	—	`Finset.uIcc` `instLatticeInt` `instLocallyFiniteOrder` `Finset.map` `Function.Embedding.trans` `Nat.castEmbedding` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `instRing` `instCharZero` `addLeftEmbedding` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `AddLeftCancelMonoid.toAddLeftCancelSemigroup` `AddCancelCommMonoid.toAddLeftCancelMonoid` `AddCommGroup.toAddCancelCommMonoid` `instAddCommGroup` `Finset.range`	—	—

---

← Back to Index