Documentation Verification Report

Box

📁 Source: Mathlib/Order/Interval/Finset/Box.lean

Statistics

Metric	Count
Definitions `Box`, `box`	2
Theorems `box_succ_disjUnion`, `box_succ_eq_sdiff`, `box_succ_union_prod`, `box_zero`, `disjoint_box_succ_prod`, `eq_zero_iff_eq_zero_of_mem_box`, `zero_mem_box`, `card_box`, `existsUnique_mem_box`, `mem_box`, `card_box_succ`	11
Total	13

BoxIntegral

Definitions

Name	Category	Theorems
`Box` 📖	CompData	143 math, 5 bridge math: `Box.splitCenterBox_le`, `Prepartition.measure_iUnion_toReal`, `Box.splitLower_def`, `TaggedPrepartition.tag_mem_Icc`, `Box.coe_coe`, `Box.splitUpper_eq_bot`, `unitPartition.mem_box_iff'`, `Box.upper_mem_Icc`, `Box.exists_mem_splitCenterBox`, `Box.measurableSet_Icc`, `Box.coe_bot`, `BoxAdditiveMap.zero_apply`, `TaggedPrepartition.filter_boxes_val`, `Box.le_TFAE`, `unitPartition.mem_prepartition_boxes_iff`, `unitPartition.mem_admissibleIndex_iff`, `Prepartition.mem_split_iff`, `Box.disjoint_withBotCoe`, `Prepartition.top_boxes`, `Box.Ioo_subset_coe`, `Box.splitUpper_le`, `unitPartition.tag_mem`, `Box.le_iff_Icc`, `Box.ext_iff`, `Box.monotone_face`, `unitPartition.box_injective`, `Prepartition.card_filter_mem_Icc_le`, `unitPartition.integralSum_eq_tsum_div`, `Prepartition.injective_boxes`, `Box.isCompact_Icc`, `TaggedPrepartition.mem_toPrepartition`, `Prepartition.mem_split_iff'`, `Box.splitUpper_def`, `Prepartition.mem_biUnion`, `Prepartition.filter_boxes`, `Box.le_iff_bounds`, `Prepartition.iUnion_def`, `BoxAdditiveMap.coe_injective`, `Prepartition.sum_fiberwise`, `Box.measure_Icc_lt_top`, `Integrable.toBoxAdditive_apply`, `Box.splitUpper_eq_self`, `MeasureTheory.AEContinuous.hasBoxIntegral`, `Prepartition.mem_restrict'`, `unitPartition.mem_box_iff`, `integrable_of_bounded_and_ae_continuous`, `BoxAdditiveMap.volume_apply`, `Prepartition.sum_biUnion_boxes`, `integral_nonneg`, `Box.coe_ae_eq_Icc`, `Prepartition.bot_boxes`, `Box.splitLower_le`, `Integrable.dist_integralSum_sum_integral_le_of_memBaseSet`, `Box.Ioo_ae_eq_Icc`, `Prepartition.distortion_biUnionTagged`, `TaggedPrepartition.mem_iUnion`, `Box.mem_splitCenterBox`, `Prepartition.mem_filter`, `Prepartition.mem_splitCenter`, `Box.lower_mem_Icc`, `Box.mem_mk`, `Box.mem_coe`, `TaggedPrepartition.mem_filter`, `norm_integral_le_of_le_const`, `Box.isSome_iff`, `Box.not_disjoint_coe_iff_nonempty_inter`, `Integrable.sum_integral_congr`, `Box.biUnion_coe_eq_coe`, `Box.Icc_def`, `integralSum_biUnionTagged`, `Prepartition.iUnion_biUnion`, `Prepartition.pairwiseDisjoint`, `Box.isBounded_Icc`, `Prepartition.sum_disj_union_boxes`, `Prepartition.IsPartition.le_iff`, `Box.monotone_upper`, `BoxAdditiveMap.toSMul_apply`, `integralSum_fiberwise`, `Box.mapsTo_insertNth_face_Icc`, `Box.splitLower_eq_bot`, `Box.coe_inf`, `Box.mk'_eq_bot`, `Box.disjoint_splitLower_splitUpper`, `Box.le_def`, `TaggedPrepartition.distortion_biUnionPrepartition`, `Prepartition.biUnion_boxes`, `Box.Ioo_subset_Icc`, `Box.exists_seq_mono_tendsto`, `Box.withBotCoe_subset_iff`, `Box.mk'_eq_coe`, `BoxAdditiveMap.map_apply`, `Prepartition.iUnion_biUnionTagged`, `hasIntegral_const`, `Box.diam_Icc_le_of_distortion_le`, `Prepartition.distortion_biUnion`, `Prepartition.IsPartition.nonempty_boxes`, `Box.disjoint_coe`, `TaggedPrepartition.IsHenstock.card_filter_tag_eq_le`, `Prepartition.injOn_setOf_mem_Icc_setOf_lower_eq`, `Prepartition.disjUnion_boxes`, `Box.splitCenterBoxEmb_apply`, `Box.mem_def`, `TaggedPrepartition.mem_infPrepartition_comm`, `Prepartition.le_iff_nonempty_imp_le_and_iUnion_subset`, `integralSum_sub_partitions`, `unitPartition.mem_prepartition_iff`, `Prepartition.iUnion_def'`, `Box.Icc_eq_pi`, `Prepartition.mem_boxes`, `MeasureTheory.Measure.toBoxAdditive_apply`, `TaggedPrepartition.disjUnion_boxes`, `unitPartition.mem_box_iff_index`, `Box.coe_subset_Icc`, `TaggedPrepartition.unionComplToSubordinate_boxes`, `integral_const`, `Box.volume_apply`, `Prepartition.disjoint_boxes_of_disjoint_iUnion`, `Prepartition.mem_inf`, `TaggedPrepartition.iUnion_def`, `Box.measurableSet_Ioo`, `Box.exists_mem`, `Prepartition.mem_restrict`, `Box.splitLower_eq_self`, `Integrable.tendsto_integralSum_sum_integral`, `BoxAdditiveMap.coe_inj`, `Box.coe_subset_coe`, `Prepartition.notMem_bot`, `Prepartition.mem_biUnionTagged`, `Prepartition.sum_split_boxes`, `unitPartition.diam_boxIcc`, `Box.upper_mem`, `Prepartition.ext_iff`, `Prepartition.biUnionIndex_le`, `Prepartition.mem_top`, `Box.mem_univ_Ioc`, `Box.injective_coe`, `Prepartition.le_def`, `Integrable.dist_integralSum_sum_integral_le_of_memBaseSet_of_iUnion_eq`, `Prepartition.mem_disjUnion`, `Box.injective_splitCenterBox`, `Prepartition.mem_iUnion`, `Box.antitone_lower`, `TaggedPrepartition.mem_disjUnion` bridge: `hasIntegralIndicatorConst`, `MeasureTheory.SimpleFunc.hasBoxIntegral`, `MeasureTheory.IntegrableOn.hasBoxIntegral`, `HasIntegral.of_aeEq_zero`, `MeasureTheory.SimpleFunc.box_integral_eq_integral`

Finset

Definitions

Name	Category	Theorems
`box` 📖	CompOp	10 math math: `box_succ_disjUnion`, `Int.card_box`, `Int.existsUnique_mem_box`, `box_succ_eq_sdiff`, `Int.mem_box`, `Prod.card_box_succ`, `disjoint_box_succ_prod`, `box_zero`, `box_succ_union_prod`, `zero_mem_box`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`box_succ_disjUnion` 📖	mathematical	—	`disjUnion` `box` `Icc` `PartialOrder.toPreorder` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Ring.toAddCommGroup` `AddMonoidWithOne.toNatCast` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `disjoint_box_succ_prod`	—	`disjoint_box_succ_prod` `disjUnion_eq_union` `box_succ_union_prod`
`box_succ_eq_sdiff` 📖	mathematical	—	`box` `Finset` `instSDiff` `Icc` `PartialOrder.toPreorder` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Ring.toAddCommGroup` `AddMonoidWithOne.toNatCast` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne`	—	`box.eq_1` `Monotone.disjointed_add_one` `Nat.instNoMaxOrder` `Nat.cast_add_one`
`box_succ_union_prod` 📖	mathematical	—	`Finset` `instUnion` `box` `Icc` `PartialOrder.toPreorder` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Ring.toAddCommGroup` `AddMonoidWithOne.toNatCast` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne`	—	`Monotone.disjointed_add_one_sup`
`box_zero` 📖	mathematical	—	`box` `Finset` `instSingleton` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing`	—	`disjointed_zero` `Nat.cast_zero` `neg_zero` `Icc_self`
`disjoint_box_succ_prod` 📖	mathematical	—	`Disjoint` `Finset` `partialOrder` `instOrderBot` `box` `Icc` `PartialOrder.toPreorder` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Ring.toAddCommGroup` `AddMonoidWithOne.toNatCast` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne`	—	`box_succ_eq_sdiff` `disjoint_sdiff_self_left`
`eq_zero_iff_eq_zero_of_mem_box` 📖	mathematical	`Finset` `instMembership` `box`	`MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing`	—	`zero_mem_box` `mem_singleton` `box_zero`
`zero_mem_box` 📖	mathematical	—	`Finset` `instMembership` `box` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing`	—	`box_zero` `box_succ_eq_sdiff` `Nat.cast_add` `Nat.cast_one` `neg_add_rev` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `IsOrderedRing.toIsOrderedAddMonoid` `zero_add` `IsOrderedRing.toZeroLEOneClass`

Int

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`card_box` 📖	mathematical	—	`Finset.card` `Finset.box` `Prod.instRing` `instRing` `Prod.instPartialOrder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `instLatticeInt` `Prod.instLocallyFiniteOrder` `PartialOrder.toPreorder` `instLocallyFiniteOrder` `Prod.instDecidableLE`	—	`Prod.card_box_succ` `IsStrictOrderedRing.toIsOrderedRing` `instIsStrictOrderedRing` `card_Icc` `sub_neg_eq_add` `Nat.cast_one` `tsub_eq_of_eq_add` `Nat.instOrderedSub` `IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `contravariant_lt_of_covariant_le` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `Nat.instAtLeastTwoHAddOfNat` `Nat.cast_mul` `Nat.cast_add` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.mul_congr` `Mathlib.Tactic.Ring.add_congr` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.cast_pos` `Mathlib.Meta.NormNum.isNat_ofNat` `Mathlib.Tactic.Ring.add_pf_add_gt` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Tactic.Ring.add_pf_add_overlap` `Mathlib.Meta.NormNum.IsNat.to_raw_eq` `Mathlib.Meta.NormNum.isNat_add` `Mathlib.Meta.NormNum.IsNat.of_raw` `Mathlib.Tactic.Ring.add_overlap_pf` `Mathlib.Tactic.Ring.add_pf_zero_add` `Mathlib.Tactic.Ring.add_mul` `Mathlib.Tactic.Ring.mul_add` `Mathlib.Meta.NormNum.isNat_mul` `Mathlib.Tactic.Ring.mul_pf_right` `Mathlib.Tactic.Ring.mul_zero` `Mathlib.Tactic.Ring.add_pf_add_lt` `Mathlib.Tactic.Ring.mul_pf_left` `Mathlib.Tactic.Ring.mul_pp_pf_overlap` `Mathlib.Tactic.Ring.zero_mul` `Mathlib.Tactic.Ring.mul_one` `Mathlib.Tactic.Ring.one_mul`
`existsUnique_mem_box` 📖	mathematical	—	`ExistsUnique` `Finset` `Finset.instMembership` `Finset.box` `Prod.instRing` `instRing` `Prod.instPartialOrder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `instLatticeInt` `Prod.instLocallyFiniteOrder` `PartialOrder.toPreorder` `instLocallyFiniteOrder` `Prod.instDecidableLE`	—	—
`mem_box` 📖	mathematical	—	`Finset` `Finset.instMembership` `Finset.box` `Prod.instRing` `instRing` `Prod.instPartialOrder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `instLatticeInt` `Prod.instLocallyFiniteOrder` `PartialOrder.toPreorder` `instLocallyFiniteOrder` `Prod.instDecidableLE`	—	`Finset.box_zero` `Finset.box_succ_eq_sdiff` `instIsOrderedRingProd` `IsStrictOrderedRing.toIsOrderedRing` `instIsStrictOrderedRing` `Nat.cast_add` `Nat.cast_one` `neg_add_rev` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `Prod.instIsOrderedAddMonoid` `instIsOrderedAddMonoid` `Prod.fst_natCast` `Prod.snd_natCast`

Prod

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`card_box_succ` 📖	mathematical	—	`Finset.card` `Finset.box` `instRing` `instPartialOrder` `instLocallyFiniteOrder` `PartialOrder.toPreorder` `Finset.Icc` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Ring.toAddCommGroup` `AddMonoidWithOne.toNatCast` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne`	—	`Finset.box_succ_eq_sdiff` `instIsOrderedRingProd` `Finset.card_sdiff_of_subset` `Finset.card_Icc_prod` `Nat.cast_add` `Nat.cast_one` `neg_add_rev` `fst_natCast` `snd_natCast`

---

← Back to Index