Proposition 7.8: if (A_j)_{j≥1} is an increasing sequence of Lebesgue measurable subsets
of ℝ^n, then m(⋃ j, A_j) is the limit of m(A_j) as j → ∞.
Proposition 7.9: if (A_j)_{j≥1} is a decreasing sequence of Lebesgue measurable subsets
of ℝ^n and the first set has finite measure, then m(⋂ j, A_j) is the limit of m(A_j) as
j → ∞ (with A 0 representing A_1).
Helper for Proposition 7.10: in dimension 0, the function-order interval
Set.Ioo does not match the coordinatewise-open-box encoding by Set.pi.
Helper for Proposition 7.10: the volume of the n = 0 open box encoded by
Set.Ioo (0-vector) ((q : ℝ)⁻¹-vector) is 0.
Helper for Proposition 7.10: the right-hand side at n = 0 is 1.
Helper for Proposition 7.10: at n = 0, the open-box equality goal is
equivalent to 0 = 1.
Helper for Proposition 7.10: in dimension 0, the open-box equality in the
current encoding is false.
Helper for Proposition 7.10: in dimension 0, the closed-box equality
in the current encoding is true.
Helper for Proposition 7.10: in dimension 0, the full conjunction is
equivalent to the open-box equality since the closed-box equality is automatic.
Helper for Proposition 7.10: in dimension 0, the full conjunction in the
current encoding is false because the open-box equality already fails.
Helper for Proposition 7.10: in dimension 0, the open-interval expression
has strictly smaller volume than the closed-interval expression.
Helper for Proposition 7.10: in dimension 0, the exact theorem-shaped
conjunction is impossible since it would force equal open/closed volumes.
Helper for Proposition 7.10: at n = 0, the full conjunction in the current
encoding is equivalent to False.
Helper for Proposition 7.10: the n = 0 branch in the exact target shape of
proposition_7_10 is equivalent to False.
Helper for Proposition 7.10: in the exact theorem-shaped n = 0 branch,
the conjunction would force (0 : ENNReal) = 1.
Helper for Proposition 7.10: in the exact theorem-shaped n = 0 branch,
the conjunction is equivalent to (0 : ENNReal) = 1.
Helper for Proposition 7.10: in the exact theorem-shaped n = 0 branch,
the open-box equality is impossible.
Helper for Proposition 7.10: in the exact theorem-shaped n = 0 branch,
the full conjunction is impossible because the open-box equality already fails.
Helper for Proposition 7.10: in the exact theorem-shaped n = 0 branch,
the conjunction is impossible.
Helper for Proposition 7.10: there exists an admissible integer q > 1
for which the current n = 0 conjunction is false.
Helper for Proposition 7.10: in dimension 0, the conjunction cannot hold
for every integer q > 1 in the current encoding.
Helper for Proposition 7.10: in dimension 0, there is no admissible
integer q > 1 for which the exact target-shaped conjunction can hold.
Helper for Proposition 7.10: for each admissible q > 1, the exact
n = 0 branch of the current target statement is false.
Helper for Proposition 7.10: for every admissible integer q > 1, the exact
n = 0 target branch in the current encoding is refutable.
Helper for Proposition 7.10: for fixed admissible q > 1, the exact
target-shaped conjunction cannot hold for every n; the n = 0 branch
already contradicts the current encoding.
Helper for Proposition 7.10: if the fully quantified current encoding held,
specializing to n = 0 and q = 2 would force (0 : ENNReal) = 1.
Helper for Proposition 7.10: the fully quantified current encoding of the
statement is false, witnessed by the n = 0, q = 2 branch.
Helper for Proposition 7.10: the closed-box identity
m([0, 1 / q]^n) = q^{-n} in the current encoding.
Helper for Proposition 7.10: when n ≠ 0, the open-interval expression
Set.Ioo (0-vector) ((q : ℝ)⁻¹-vector) has the same volume as the closed box.
Helper for Proposition 7.10: when n ≠ 0, the open-interval expression
Set.Ioo (0-vector) ((q : ℝ)⁻¹-vector) has the same volume as the closed box,
so it also has measure q^{-n}.
Helper for Proposition 7.10: when n ≠ 0, both the open-box and closed-box
volume identities hold in the current encoding.
Helper for Proposition 7.10: in the n = 0 branch of the current encoding,
any target-shaped conjunction contradicts the admissibility hypothesis q > 1.
Helper for Proposition 7.10: with q > 1, the exact n = 0 target branch
of proposition_7_10 is equivalent to False in the current encoding.
Helper for Proposition 7.10: in the current encoding, any witness of the
exact target-shaped conjunction forces n ≠ 0, independently of hypotheses on
q.
Helper for Proposition 7.10: for q > 1, any witness of the exact target
conjunction must come from a nonzero dimension.
Helper for Proposition 7.10: for q > 1, even the open-box equality alone
in the current encoding forces the dimension to be nonzero.
Helper for Proposition 7.10: if the exact target-shaped conjunction holds
and one also assumes n = 0, this yields a contradiction.
Helper for Proposition 7.10: for q > 1, the exact target-shaped conjunction
in dimension n is equivalent to n ≠ 0 in the current encoding.
Helper for Proposition 7.10: if n = 0 and q > 1, the target-shaped
conjunction for dimension n yields a contradiction in the current encoding.
Helper for Proposition 7.10: for every admissible q > 1, the exact
theorem-shaped n = 0 conjunction is unsatisfiable in the current encoding.
Helper for Proposition 7.10: in dimension 0, the open-box equality in the
current encoding fails, while the closed-box equality holds.
Helper for Proposition 7.10: in dimension 0, any witness of the exact
theorem-shaped conjunction forces the arithmetic constraint q ≤ 1.
Helper for Proposition 7.10: any witness of the exact theorem-shaped
n = 0 branch forces failure of the admissibility condition q > 1.
Helper for Proposition 7.10: for each admissible q > 1, the exact
n = 0 conjunction required by the current target statement is not inhabited.
Helper for Proposition 7.10: the fully quantified theorem-shaped statement in
the current encoding is inconsistent, witnessed by n = 0 and q = 2.
Helper for Proposition 7.10: when q > 1, the exact theorem-shaped
n = 0 branch type is empty in the current encoding.
Helper for Proposition 7.10: in positive dimension, the target conjunction follows from the nonzero-dimension case.
Proposition 7.10: for positive dimension n and q ∈ ℤ with q > 1, the
open box (0, 1 / q)^n = {x : ℝ^n | 0 < x_j < 1 / q for all j} and the closed
box [0, 1 / q]^n = {x : ℝ^n | 0 ≤ x_j ≤ 1 / q for all j} have Lebesgue
measure q^{-n}.
Proposition 7.11: for an axis-parallel closed box
B = ∏ i, [a i, b i] ⊆ ℝ^n with a i ≤ b i, the set B is Lebesgue measurable and
its Lebesgue measure equals its box volume ∏ i, (b i - a i).