Let p be a predicate on box ι, let I be a box. Suppose that the following two properties hold true.

• Consider a smaller box J ≤ I. The hyperplanes passing through the center of J split it into 2 ^ n boxes. If p holds true on each of these boxes, then it true on J.
• For each z in the closed box I.Icc there exists a neighborhood U of z within I.Icc such that for every box J ≤ I such that z ∈ J.Icc ⊆ U, if J is homothetic to I with a coefficient of the form 1 / 2 ^ m, then p is true on J.

Then p I is true. See also box_integral.box.subbox_induction_on' for a version using box_integral.box.split_center_box instead of box_integral.prepartition.split_center.

Given a box I in ℝⁿ and a function r : ℝⁿ → (0, ∞), there exists a tagged partition π of I such that

• π is a Henstock partition;
• π is subordinate to r;
• each box in π is homothetic to I with coefficient of the form 1 / 2 ^ m.

This lemma implies that the Henstock filter is nontrivial, hence the Henstock integral is well-defined.

Given a box I in ℝⁿ, a function r : ℝⁿ → (0, ∞), and a prepartition π of I, there exists a tagged prepartition π' of I such that

• each box of π' is included in some box of π;
• π' is a Henstock partition;
• π' is subordinate to r;
• π' covers exactly the same part of I as π;
• the distortion of π' is equal to the distortion of π.