SubboxInduction

📁 Source: Mathlib/Analysis/BoxIntegral/Partition/SubboxInduction.lean

Statistics

Metric	Count
Definitions splitCenter, toSubordinate, unionComplToSubordinate	3
Theorems exists_taggedPartition_isHenstock_isSubordinate_homothetic, subbox_induction_on, distortion_toSubordinate, exists_tagged_le_isHenstock_isSubordinate_iUnion_eq, iUnion_toSubordinate, isHenstock_toSubordinate, isPartition_splitCenter, isSubordinate_toSubordinate, mem_splitCenter, toSubordinate_toPrepartition_le, upper_sub_lower_of_mem_splitCenter, distortion_unionComplToSubordinate, iUnion_unionComplToSubordinate_boxes, isPartition_unionComplToSubordinate, unionComplToSubordinate_boxes	15
Total	18

BoxIntegral.Box

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exists_taggedPartition_isHenstock_isSubordinate_homothetic 📖	mathematical	—	BoxIntegral.TaggedPrepartition.IsPartition BoxIntegral.TaggedPrepartition.IsHenstock BoxIntegral.TaggedPrepartition.IsSubordinate Real Real.instSub upper lower DivInvMonoid.toDiv Real.instDivInvMonoid Monoid.toNatPow Real.instMonoid instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat BoxIntegral.TaggedPrepartition.distortion distortion	—	subbox_induction_on Nat.instAtLeastTwoHAddOfNat BoxIntegral.Prepartition.IsPartition.biUnionTagged BoxIntegral.Prepartition.isPartition_splitCenter BoxIntegral.Prepartition.mem_biUnionTagged BoxIntegral.Prepartition.upper_sub_lower_of_mem_splitCenter div_div pow_succ' BoxIntegral.TaggedPrepartition.isHenstock_biUnionTagged BoxIntegral.TaggedPrepartition.isSubordinate_biUnionTagged BoxIntegral.TaggedPrepartition.distortion_of_const BoxIntegral.Prepartition.IsPartition.nonempty_boxes distortion_eq_of_sub_eq_div Function.sometimes_spec inter_mem_nhdsWithin Metric.closedBall_mem_nhds Subtype.coe_prop le_rfl BoxIntegral.TaggedPrepartition.isPartition_single BoxIntegral.TaggedPrepartition.isHenstock_single BoxIntegral.TaggedPrepartition.isSubordinate_single Set.subset_inter_iff pow_zero div_one BoxIntegral.TaggedPrepartition.distortion_single
subbox_induction_on 📖	—	Set Filter Filter.instMembership nhdsWithin Pi.topologicalSpace Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace DFunLike.coe OrderEmbedding BoxIntegral.Box instLE Set.instLE instFunLikeOrderEmbedding Icc	—	—	Nat.instAtLeastTwoHAddOfNat subbox_induction_on' BoxIntegral.Prepartition.mem_splitCenter

BoxIntegral.Prepartition

Definitions

Name	Category	Theorems
splitCenter 📖	CompOp	2 math math: mem_splitCenter, isPartition_splitCenter
toSubordinate 📖	CompOp	6 math math: isSubordinate_toSubordinate, isHenstock_toSubordinate, BoxIntegral.TaggedPrepartition.unionComplToSubordinate_boxes, toSubordinate_toPrepartition_le, iUnion_toSubordinate, distortion_toSubordinate

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
distortion_toSubordinate 📖	mathematical	—	BoxIntegral.TaggedPrepartition.distortion toSubordinate distortion	—	exists_tagged_le_isHenstock_isSubordinate_iUnion_eq
exists_tagged_le_isHenstock_isSubordinate_iUnion_eq 📖	mathematical	—	BoxIntegral.Prepartition instLE BoxIntegral.TaggedPrepartition.toPrepartition BoxIntegral.TaggedPrepartition.IsHenstock BoxIntegral.TaggedPrepartition.IsSubordinate BoxIntegral.TaggedPrepartition.distortion distortion BoxIntegral.TaggedPrepartition.iUnion iUnion	—	Nat.instAtLeastTwoHAddOfNat BoxIntegral.Box.exists_taggedPartition_isHenstock_isSubordinate_homothetic biUnion_le BoxIntegral.TaggedPrepartition.isHenstock_biUnionTagged BoxIntegral.TaggedPrepartition.isSubordinate_biUnionTagged distortion_biUnionTagged Finset.sup_congr iUnion_biUnion_partition
iUnion_toSubordinate 📖	mathematical	—	BoxIntegral.TaggedPrepartition.iUnion toSubordinate iUnion	—	exists_tagged_le_isHenstock_isSubordinate_iUnion_eq
isHenstock_toSubordinate 📖	mathematical	—	BoxIntegral.TaggedPrepartition.IsHenstock toSubordinate	—	exists_tagged_le_isHenstock_isSubordinate_iUnion_eq
isPartition_splitCenter 📖	mathematical	—	IsPartition splitCenter	—	—
isSubordinate_toSubordinate 📖	mathematical	—	BoxIntegral.TaggedPrepartition.IsSubordinate toSubordinate	—	exists_tagged_le_isHenstock_isSubordinate_iUnion_eq
mem_splitCenter 📖	mathematical	—	BoxIntegral.Box BoxIntegral.Prepartition instMembershipBox splitCenter BoxIntegral.Box.splitCenterBox	—	—
toSubordinate_toPrepartition_le 📖	mathematical	—	BoxIntegral.Prepartition instLE BoxIntegral.TaggedPrepartition.toPrepartition toSubordinate	—	exists_tagged_le_isHenstock_isSubordinate_iUnion_eq
upper_sub_lower_of_mem_splitCenter 📖	mathematical	BoxIntegral.Box BoxIntegral.Prepartition instMembershipBox splitCenter	Real Real.instSub BoxIntegral.Box.upper BoxIntegral.Box.lower DivInvMonoid.toDiv Real.instDivInvMonoid instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat	—	Nat.instAtLeastTwoHAddOfNat mem_splitCenter BoxIntegral.Box.upper_sub_lower_splitCenterBox

BoxIntegral.TaggedPrepartition

Definitions

Name	Category	Theorems
unionComplToSubordinate 📖	CompOp	5 math math: iUnion_unionComplToSubordinate_boxes, isPartition_unionComplToSubordinate, BoxIntegral.IntegrationParams.MemBaseSet.unionComplToSubordinate, unionComplToSubordinate_boxes, distortion_unionComplToSubordinate

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
distortion_unionComplToSubordinate 📖	mathematical	BoxIntegral.Prepartition.iUnion Set Set.instSDiff BoxIntegral.Box.toSet iUnion	distortion unionComplToSubordinate NNReal NNReal.instMax BoxIntegral.Prepartition.distortion	—	distortion_disjUnion BoxIntegral.Prepartition.distortion_toSubordinate
iUnion_unionComplToSubordinate_boxes 📖	mathematical	BoxIntegral.Prepartition.iUnion Set Set.instSDiff BoxIntegral.Box.toSet iUnion	unionComplToSubordinate	—	BoxIntegral.Prepartition.IsPartition.iUnion_eq isPartition_unionComplToSubordinate
isPartition_unionComplToSubordinate 📖	mathematical	BoxIntegral.Prepartition.iUnion Set Set.instSDiff BoxIntegral.Box.toSet iUnion	IsPartition unionComplToSubordinate	—	BoxIntegral.Prepartition.isPartitionDisjUnionOfEqDiff BoxIntegral.Prepartition.iUnion_toSubordinate
unionComplToSubordinate_boxes 📖	mathematical	BoxIntegral.Prepartition.iUnion Set Set.instSDiff BoxIntegral.Box.toSet iUnion	BoxIntegral.Prepartition.boxes toPrepartition unionComplToSubordinate Finset BoxIntegral.Box Finset.instUnion BoxIntegral.Prepartition.toSubordinate	—	—

---

← Back to Index