Box 📖 | CompData | 181 math, 7 bridgemath: Box.splitCenterBox_le, BoxAdditiveMap.map_split_add, 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.face_mono, Box.measurableSet_Icc, Box.coe_bot, BoxAdditiveMap.zero_apply, TaggedPrepartition.filter_boxes_val, Box.le_TFAE, Prepartition.le_of_mem, unitPartition.mem_prepartition_boxes_iff, TaggedPrepartition.isHenstock_single, 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, integrable_of_continuousOn, Prepartition.card_filter_mem_Icc_le, unitPartition.integralSum_eq_tsum_div, Prepartition.injective_boxes, Prepartition.IsPartition.existsUnique, Box.isCompact_Icc, TaggedPrepartition.mem_toPrepartition, Prepartition.mem_split_iff', Box.splitUpper_def, Prepartition.mem_biUnion, Prepartition.filter_boxes, Prepartition.biUnionIndex_mem, Box.le_iff_bounds, TaggedPrepartition.mem_mk, Prepartition.iUnion_def, BoxAdditiveMap.coe_injective, TaggedPrepartition.isSubordinate_single, Prepartition.sum_fiberwise, Box.measure_Icc_lt_top, Integrable.toBoxAdditive_apply, Box.splitUpper_eq_self, MeasureTheory.AEContinuous.hasBoxIntegral, Prepartition.mem_single, Box.iUnion_Ioo_of_tendsto, Prepartition.mem_restrict', BoxAdditiveMap.upperSubLower_apply, Prepartition.mem_mk, 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, Prepartition.le_biUnionIndex, Box.mem_splitCenterBox, Prepartition.mem_filter, Prepartition.mem_splitCenter, Box.continuousOn_face_Icc, Box.lower_mem_Icc, Box.mem_mk, Box.mem_coe, TaggedPrepartition.isHenstock_single_iff, 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, BoxAdditiveMap.coe_mk, 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, le_hasIntegralVertices_of_isBounded, Box.disjoint_splitLower_splitUpper, Box.le_def, TaggedPrepartition.distortion_biUnionPrepartition, Prepartition.biUnion_boxes, Box.Ioo_subset_Icc, BoxAdditiveMap.sum_partition_boxes, Box.exists_seq_mono_tendsto, MeasureTheory.ContinuousOn.hasBoxIntegral, 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, HasIntegral.of_le_Henstock_of_forall_isLittleO, Prepartition.IsPartition.nonempty_boxes, Box.disjoint_coe, Prepartition.single_boxes, TaggedPrepartition.IsHenstock.card_filter_tag_eq_le, Prepartition.injOn_setOf_mem_Icc_setOf_lower_eq, Prepartition.disjUnion_boxes, TaggedPrepartition.IsSubordinate.diam_le, 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, Prepartition.mem_ofWithBot, TaggedPrepartition.single_boxes_val, Box.coe_subset_Icc, TaggedPrepartition.unionComplToSubordinate_boxes, integral_const, Prepartition.le_of_mem', 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, Prepartition.iUnion_ofWithBot, integrable_of_bounded_and_ae_continuousWithinAt, Box.coe_subset_coe, Prepartition.notMem_bot, Prepartition.mem_biUnionTagged, norm_integral_le_of_norm_le, Prepartition.sum_split_boxes, BoxAdditiveMap.sum_partition_boxes', Prepartition.not_disjoint_imp_le_of_subset_of_mem_splitMany, TaggedPrepartition.mem_single, unitPartition.diam_boxIcc, Prepartition.mem_biUnionIndex, Box.upper_mem, HasIntegral.mcShane_of_forall_isLittleO, Prepartition.ext_iff, BoxAdditiveMap.sum_boxes_congr, Prepartition.biUnionIndex_le, Prepartition.mem_top, BoxAdditiveMap.restrict_apply, 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.isPartition_single, Prepartition.sum_ofWithBot, TaggedPrepartition.mem_disjUnion
bridge: hasIntegralIndicatorConst, MeasureTheory.SimpleFunc.hasBoxIntegral, MeasureTheory.IntegrableOn.hasBoxIntegral, HasIntegral.of_bRiemann_eq_false_of_forall_isLittleO, HasIntegral.of_aeEq_zero, HasIntegral.congr_ae, MeasureTheory.SimpleFunc.box_integral_eq_integral
|