theorem helperForProposition_7_2_closedBox_outer_le_thickened {d : ℕ} (a b : Fin (d + 1) → ℝ) (h : ∀ (i : Fin (d + 1)), a i ≤ b i) {ε : ℝ} (hε : 0 < ε) : (boxOuterMeasure (d + 1)) (Set.Icc a b) ≤ ENNReal.ofReal (∏ i : Fin (d + 1), (b i - a i + 2 * ε))

Helper for Proposition 7.2: thickening each side of a closed box by ε gives an explicit upper bound for boxOuterMeasure.

theorem helperForProposition_7_2_closedBox_outer_le_volume {d : ℕ} (a b : Fin (d + 1) → ℝ) (h : ∀ (i : Fin (d + 1)), a i ≤ b i) : (boxOuterMeasure (d + 1)) (Set.Icc a b) ≤ ENNReal.ofReal (∏ i : Fin (d + 1), (b i - a i))

Helper for Proposition 7.2: removing the thickening parameter yields the sharp closed-box upper bound for boxOuterMeasure in positive dimension.

theorem proposition_7_2 (n : ℕ) (_hn : 0 < n) (a b : Fin n → ℝ) (h : ∀ (i : Fin n), a i ≤ b i) : (boxOuterMeasure n) (Set.Icc a b) = ENNReal.ofReal (∏ i : Fin n, (b i - a i))

Proposition 7.2 (Outer measure of a closed box, positive dimension): if B = ∏ i, [a i, b i] ⊆ ℝ^n with 0 < n and a i ≤ b i for all i, then the box outer measure satisfies m*(B) = ∏ i, (b i - a i).

theorem helperForTheorem_7_2_zeroDim_not_lt (a b : Fin 0 → ℝ) : ¬a < b

Helper for Theorem 7.2: in dimension 0, strict order between functions is impossible.

theorem helperForTheorem_7_2_zeroDim_Ioo_eq_empty (a b : Fin 0 → ℝ) : Set.Ioo a b = ∅

Helper for Theorem 7.2: in dimension 0, every open box Set.Ioo a b is empty.

theorem helperForTheorem_7_2_zeroDim_outer_eq_zero (a b : Fin 0 → ℝ) : (boxOuterMeasure 0) (Set.Ioo a b) = 0

Helper for Theorem 7.2: in dimension 0, the open-box outer measure is zero.

theorem helperForTheorem_7_2_zeroDim_rhs_eq_one (a b : Fin 0 → ℝ) : ENNReal.ofReal (∏ i : Fin 0, (b i - a i)) = 1

Helper for Theorem 7.2: in dimension 0, the right-hand side product equals one.

theorem helperForTheorem_7_2_zeroDim_outer_lt_rhs (a b : Fin 0 → ℝ) : (boxOuterMeasure 0) (Set.Ioo a b) < ENNReal.ofReal (∏ i : Fin 0, (b i - a i))

Helper for Theorem 7.2: in dimension 0, the left side is strictly smaller than the right side in the target equality.

theorem helperForTheorem_7_2_zeroDim_rhs_sub_outer_eq_one (a b : Fin 0 → ℝ) : ENNReal.ofReal (∏ i : Fin 0, (b i - a i)) - (boxOuterMeasure 0) (Set.Ioo a b) = 1

Helper for Theorem 7.2: in dimension 0, the right-hand side minus the left-hand side equals 1, quantitatively witnessing the gap in the target formula.

theorem helperForTheorem_7_2_zeroDim_rhs_ne_zero (a b : Fin 0 → ℝ) : ENNReal.ofReal (∏ i : Fin 0, (b i - a i)) ≠ 0

Helper for Theorem 7.2: in dimension 0, the right-hand side product is nonzero.

theorem helperForTheorem_7_2_zeroDim_targetEq_iff_rhs_eq_zero (a b : Fin 0 → ℝ) : (boxOuterMeasure 0) (Set.Ioo a b) = ENNReal.ofReal (∏ i : Fin 0, (b i - a i)) ↔ ENNReal.ofReal (∏ i : Fin 0, (b i - a i)) = 0

Helper for Theorem 7.2: in dimension 0, the target equality is equivalent to the right-hand side being 0.

theorem helperForTheorem_7_2_zeroDim_formula_false (a b : Fin 0 → ℝ) : (boxOuterMeasure 0) (Set.Ioo a b) ≠ ENNReal.ofReal (∏ i : Fin 0, (b i - a i))

Helper for Theorem 7.2: the zero-dimensional specialization of the open-box formula is false for the current outer-measure model.

theorem helperForTheorem_7_2_zeroDim_counterexample : ∃ (a : Fin 0 → ℝ) (b : Fin 0 → ℝ), (∀ (i : Fin 0), a i ≤ b i) ∧ (boxOuterMeasure 0) (Set.Ioo a b) ≠ ENNReal.ofReal (∏ i : Fin 0, (b i - a i))

Helper for Theorem 7.2: there is an explicit zero-dimensional pair (a, b) satisfying the order hypothesis while refuting the target open-box equality.

theorem helperForTheorem_7_2_zeroDim_eq_implies_false (a b : Fin 0 → ℝ) (hEq : (boxOuterMeasure 0) (Set.Ioo a b) = ENNReal.ofReal (∏ i : Fin 0, (b i - a i))) : False

Helper for Theorem 7.2: any claimed zero-dimensional open-box equality yields a contradiction in the current normalization.

theorem helperForTheorem_7_2_zeroDim_le_vacuous (a b : Fin 0 → ℝ) (i : Fin 0) : a i ≤ b i

Helper for Theorem 7.2: in dimension 0, the hypothesis a i ≤ b i is vacuous.

theorem helperForTheorem_7_2_zeroDim_le_iff_true (a b : Fin 0 → ℝ) : (∀ (i : Fin 0), a i ≤ b i) ↔ True

Helper for Theorem 7.2: in dimension 0, the coordinatewise order hypothesis is equivalent to True.

theorem helperForTheorem_7_2_zeroDim_forallAB_formula_false : ¬∀ (a b : Fin 0 → ℝ), (∀ (i : Fin 0), a i ≤ b i) → (boxOuterMeasure 0) (Set.Ioo a b) = ENNReal.ofReal (∏ i : Fin 0, (b i - a i))

Helper for Theorem 7.2: in dimension 0, a formula claiming the target open-box equality for every pair (a, b) is inconsistent with the model.

theorem helperForTheorem_7_2_global_formula_implies_zero_eq_one (hAll : ∀ (n : ℕ) (a b : Fin n → ℝ), (∀ (i : Fin n), a i ≤ b i) → (boxOuterMeasure n) (Set.Ioo a b) = ENNReal.ofReal (∏ i : Fin n, (b i - a i))) : 0 = 1

Helper for Theorem 7.2: any fully quantified open-box formula forces (0 : ENNReal) = 1 by specializing to dimension 0.

theorem helperForTheorem_7_2_global_formula_false : ¬∀ (n : ℕ) (a b : Fin n → ℝ), (∀ (i : Fin n), a i ≤ b i) → (boxOuterMeasure n) (Set.Ioo a b) = ENNReal.ofReal (∏ i : Fin n, (b i - a i))

Helper for Theorem 7.2: the fully quantified open-box formula is impossible in the current model because the n = 0 instance contradicts 0 ≠ 1.

theorem helperForTheorem_7_2_positiveDim_selfSub_prod_eq_zero {n : ℕ} (hn : 0 < n) (a : Fin n → ℝ) : ENNReal.ofReal (∏ i : Fin n, (a i - a i)) = 0

Helper for Theorem 7.2: in positive dimension, the self-difference product vanishes.

theorem helperForTheorem_7_2_positiveDim_singleton_outer_eq_zero {n : ℕ} (hn : 0 < n) (x : Fin n → ℝ) : (boxOuterMeasure n) {x} = 0

Helper for Theorem 7.2: in positive dimension, each singleton has boxOuterMeasure zero.

theorem helperForTheorem_7_2_positiveDim_endpoints_outer_eq_zero {n : ℕ} (hn : 0 < n) (a b : Fin n → ℝ) : (boxOuterMeasure n) ({a} ∪ {b}) = 0

Helper for Theorem 7.2: in positive dimension, removing the two endpoints a and b costs zero outer measure.

theorem helperForTheorem_7_2_Icc_subset_Ioo_union_endpoints {n : ℕ} (a b : Fin n → ℝ) : Set.Icc a b ⊆ Set.Ioo a b ∪ ({a} ∪ {b})

Helper for Theorem 7.2: every point of Set.Icc a b is either in Set.Ioo a b or is one of the two endpoints.

theorem helperForTheorem_7_2_outer_Ioo_le_outer_Icc {n : ℕ} (a b : Fin n → ℝ) : (boxOuterMeasure n) (Set.Ioo a b) ≤ (boxOuterMeasure n) (Set.Icc a b)

Helper for Theorem 7.2: monotonicity gives the easy inequality boxOuterMeasure n (Set.Ioo a b) ≤ boxOuterMeasure n (Set.Icc a b).

theorem helperForTheorem_7_2_positiveDim_outer_Ioo_eq_outer_Icc {n : ℕ} (hn : 0 < n) (a b : Fin n → ℝ) : (boxOuterMeasure n) (Set.Ioo a b) = (boxOuterMeasure n) (Set.Icc a b)

Helper for Theorem 7.2: in positive dimension, Set.Ioo a b and Set.Icc a b have the same box outer measure.

theorem helperForTheorem_7_2_positiveDim_openBox_eq {n : ℕ} (hn : 0 < n) (a b : Fin n → ℝ) (h : ∀ (i : Fin n), a i ≤ b i) : (boxOuterMeasure n) (Set.Ioo a b) = ENNReal.ofReal (∏ i : Fin n, (b i - a i))

Helper for Theorem 7.2: the open-box outer-measure formula holds in positive dimension.

theorem helperForTheorem_7_2_zeroDim_targetEq_iff_zero_eq_one (a b : Fin 0 → ℝ) : (boxOuterMeasure 0) (Set.Ioo a b) = ENNReal.ofReal (∏ i : Fin 0, (b i - a i)) ↔ 0 = 1

Helper for Theorem 7.2: in dimension 0, the target open-box equality is equivalent to the impossible equality 0 = 1 in ENNReal.

theorem helperForTheorem_7_2_zeroDim_targetEq_iff_false (a b : Fin 0 → ℝ) : (boxOuterMeasure 0) (Set.Ioo a b) = ENNReal.ofReal (∏ i : Fin 0, (b i - a i)) ↔ False

Helper for Theorem 7.2: in dimension 0, the target open-box equality is equivalent to False.

theorem helperForTheorem_7_2_zeroDim_targetEq_implies_zero_eq_one (a b : Fin 0 → ℝ) (hEq : (boxOuterMeasure 0) (Set.Ioo a b) = ENNReal.ofReal (∏ i : Fin 0, (b i - a i))) : 0 = 1

Helper for Theorem 7.2: in dimension 0, any proof of the target equality forces the contradictory identity 0 = 1 in ENNReal.

theorem helperForTheorem_7_2_zeroDim_targetEq_implies_false_via_sub (a b : Fin 0 → ℝ) (hEq : (boxOuterMeasure 0) (Set.Ioo a b) = ENNReal.ofReal (∏ i : Fin 0, (b i - a i))) : False

Helper for Theorem 7.2: in dimension 0, any proof of the target equality forces the quantitative gap rhs - lhs to be simultaneously 0 and 1, hence impossible.

theorem helperForTheorem_7_2_zeroDim_targetEq_not (a b : Fin 0 → ℝ) : ¬(boxOuterMeasure 0) (Set.Ioo a b) = ENNReal.ofReal (∏ i : Fin 0, (b i - a i))

Helper for Theorem 7.2: in dimension 0, the target equality is refutable.

theorem helperForTheorem_7_2_zeroDim_hypothesis_does_not_rescue_target (a b : Fin 0 → ℝ) : ¬((∀ (i : Fin 0), a i ≤ b i) → (boxOuterMeasure 0) (Set.Ioo a b) = ENNReal.ofReal (∏ i : Fin 0, (b i - a i)))

Helper for Theorem 7.2: even with the vacuous order hypothesis in dimension 0, the target open-box equality cannot be obtained.

theorem helperForTheorem_7_2_zeroDim_le_and_targetEq_implies_false (a b : Fin 0 → ℝ) (hLe : ∀ (i : Fin 0), a i ≤ b i) (hEq : (boxOuterMeasure 0) (Set.Ioo a b) = ENNReal.ofReal (∏ i : Fin 0, (b i - a i))) : False

Helper for Theorem 7.2: in dimension 0, combining the vacuous order hypothesis with the target equality yields a contradiction.

theorem helperForTheorem_7_2_zeroDim_targetEq_iff_false_of_le (a b : Fin 0 → ℝ) (h : ∀ (i : Fin 0), a i ≤ b i) : (boxOuterMeasure 0) (Set.Ioo a b) = ENNReal.ofReal (∏ i : Fin 0, (b i - a i)) ↔ False

Helper for Theorem 7.2: in dimension 0, under the order hypothesis, the target open-box equality is equivalent to False.

theorem helperForTheorem_7_2_zeroDim_targetEq_not_of_le (a b : Fin 0 → ℝ) (h : ∀ (i : Fin 0), a i ≤ b i) : ¬(boxOuterMeasure 0) (Set.Ioo a b) = ENNReal.ofReal (∏ i : Fin 0, (b i - a i))

Helper for Theorem 7.2: in dimension 0, the order hypothesis implies the target open-box equality is impossible.

theorem helperForTheorem_7_2_zeroDim_le_and_targetEq_iff_false (a b : Fin 0 → ℝ) : (∀ (i : Fin 0), a i ≤ b i) ∧ (boxOuterMeasure 0) (Set.Ioo a b) = ENNReal.ofReal (∏ i : Fin 0, (b i - a i)) ↔ False

Helper for Theorem 7.2: in dimension 0, the conjunction of the order hypothesis and the target equality is equivalent to False.

theorem helperForTheorem_7_2_zeroDim_no_box_satisfies_hypothesis_and_targetEq : ¬∃ (a : Fin 0 → ℝ) (b : Fin 0 → ℝ), (∀ (i : Fin 0), a i ≤ b i) ∧ (boxOuterMeasure 0) (Set.Ioo a b) = ENNReal.ofReal (∏ i : Fin 0, (b i - a i))

Helper for Theorem 7.2: in dimension 0, no pair of endpoints can satisfy both the order hypothesis and the target equality.

theorem helperForTheorem_7_2_zeroDim_no_hypothesis_witness_for_targetEq (a b : Fin 0 → ℝ) : ¬∃ (_ : ∀ (i : Fin 0), a i ≤ b i), (boxOuterMeasure 0) (Set.Ioo a b) = ENNReal.ofReal (∏ i : Fin 0, (b i - a i))

Helper for Theorem 7.2: for fixed a, b : Fin 0 → ℝ, there is no witness h : ∀ i, a i ≤ b i for which the target open-box equality holds.

theorem helperForTheorem_7_2_zeroDim_not_targetEq_of_noWitness (a b : Fin 0 → ℝ) (h : ∀ (i : Fin 0), a i ≤ b i) (hNoWitness : ¬∃ (_ : ∀ (i : Fin 0), a i ≤ b i), (boxOuterMeasure 0) (Set.Ioo a b) = ENNReal.ofReal (∏ i : Fin 0, (b i - a i))) : ¬(boxOuterMeasure 0) (Set.Ioo a b) = ENNReal.ofReal (∏ i : Fin 0, (b i - a i))

Helper for Theorem 7.2: in dimension 0, once witness nonexistence is known, any fixed order hypothesis immediately rules out the target equality.

theorem helperForTheorem_7_2_universal_target_statement_implies_false (hAll : ∀ (n : ℕ) (a b : Fin n → ℝ), (∀ (i : Fin n), a i ≤ b i) → (boxOuterMeasure n) (Set.Ioo a b) = ENNReal.ofReal (∏ i : Fin n, (b i - a i))) : False

Helper for Theorem 7.2: any proof of the fully quantified open-box formula immediately yields a contradiction in this model.

theorem helperForTheorem_7_2_zeroDim_targetEq_implies_one_eq_zero (a b : Fin 0 → ℝ) (hEq : (boxOuterMeasure 0) (Set.Ioo a b) = ENNReal.ofReal (∏ i : Fin 0, (b i - a i))) : 1 = 0

Helper for Theorem 7.2: in dimension 0, any proof of the target equality forces the contradiction (1 : ENNReal) = 0.

theorem helperForTheorem_7_2_universal_target_statement_not : ¬∀ (n : ℕ) (a b : Fin n → ℝ), (∀ (i : Fin n), a i ≤ b i) → (boxOuterMeasure n) (Set.Ioo a b) = ENNReal.ofReal (∏ i : Fin n, (b i - a i))

Helper for Theorem 7.2: the fully quantified open-box target statement is false in this model.

theorem helperForTheorem_7_2_targetEq_not_of_eq_zero_dim {n : ℕ} (hn : n = 0) (a b : Fin n → ℝ) (h : ∀ (i : Fin n), a i ≤ b i) : ¬(boxOuterMeasure n) (Set.Ioo a b) = ENNReal.ofReal (∏ i : Fin n, (b i - a i))

Helper for Theorem 7.2: if the ambient dimension is identified with 0, the target open-box equality is impossible under the coordinatewise order hypothesis.

theorem helperForTheorem_7_2_targetLt_of_not_pos_dim {n : ℕ} (hn : ¬0 < n) (a b : Fin n → ℝ) : (boxOuterMeasure n) (Set.Ioo a b) < ENNReal.ofReal (∏ i : Fin n, (b i - a i))

Helper for Theorem 7.2: if the ambient dimension is not positive, then in fact the left side is strictly smaller than the right side in the target formula.

theorem helperForTheorem_7_2_target_rhs_sub_outer_eq_one_of_not_pos_dim {n : ℕ} (hn : ¬0 < n) (a b : Fin n → ℝ) : ENNReal.ofReal (∏ i : Fin n, (b i - a i)) - (boxOuterMeasure n) (Set.Ioo a b) = 1

Helper for Theorem 7.2: in nonpositive dimension, the quantitative gap rhs - lhs in the target formula equals 1.

theorem helperForTheorem_7_2_target_rhs_sub_outer_ne_zero_of_not_pos_dim {n : ℕ} (hn : ¬0 < n) (a b : Fin n → ℝ) : ENNReal.ofReal (∏ i : Fin n, (b i - a i)) - (boxOuterMeasure n) (Set.Ioo a b) ≠ 0

Helper for Theorem 7.2: in nonpositive dimension, the quantitative gap rhs - lhs in the target formula is nonzero.

theorem helperForTheorem_7_2_targetEq_implies_false_of_not_pos_dim_via_sub {n : ℕ} (hn : ¬0 < n) (a b : Fin n → ℝ) (hEq : (boxOuterMeasure n) (Set.Ioo a b) = ENNReal.ofReal (∏ i : Fin n, (b i - a i))) : False

Helper for Theorem 7.2: in nonpositive dimension, any claimed target equality forces a contradiction via rhs - lhs = 0 versus rhs - lhs = 1.

theorem helperForTheorem_7_2_targetEq_not_of_not_pos_dim {n : ℕ} (hn : ¬0 < n) (a b : Fin n → ℝ) (h : ∀ (i : Fin n), a i ≤ b i) : ¬(boxOuterMeasure n) (Set.Ioo a b) = ENNReal.ofReal (∏ i : Fin n, (b i - a i))

Helper for Theorem 7.2: if the ambient dimension is not positive, then the target open-box equality is impossible under the coordinatewise order hypothesis.

theorem helperForTheorem_7_2_not_pos_dim_le_and_targetEq_iff_false {n : ℕ} (hn : ¬0 < n) (a b : Fin n → ℝ) : (∀ (i : Fin n), a i ≤ b i) ∧ (boxOuterMeasure n) (Set.Ioo a b) = ENNReal.ofReal (∏ i : Fin n, (b i - a i)) ↔ False

Helper for Theorem 7.2: in nonpositive dimension, the order hypothesis and the target open-box equality are jointly equivalent to False.

theorem helperForTheorem_7_2_not_pos_dim_no_hypothesis_witness_for_targetEq {n : ℕ} (hn : ¬0 < n) (a b : Fin n → ℝ) : ¬∃ (_ : ∀ (i : Fin n), a i ≤ b i), (boxOuterMeasure n) (Set.Ioo a b) = ENNReal.ofReal (∏ i : Fin n, (b i - a i))

Helper for Theorem 7.2: in nonpositive dimension, there is no order-hypothesis h witnessing the target open-box equality.

theorem helperForTheorem_7_2_targetEq_iff_pos_dim {n : ℕ} (a b : Fin n → ℝ) (h : ∀ (i : Fin n), a i ≤ b i) : (boxOuterMeasure n) (Set.Ioo a b) = ENNReal.ofReal (∏ i : Fin n, (b i - a i)) ↔ 0 < n

Helper for Theorem 7.2: for fixed endpoints satisfying the order hypothesis, the target open-box equality holds exactly in positive dimension.

theorem helperForTheorem_7_2_targetEq_iff_false_of_not_pos_dim {n : ℕ} (hn : ¬0 < n) (a b : Fin n → ℝ) (h : ∀ (i : Fin n), a i ≤ b i) : (boxOuterMeasure n) (Set.Ioo a b) = ENNReal.ofReal (∏ i : Fin n, (b i - a i)) ↔ False

Helper for Theorem 7.2: in nonpositive dimension, the target open-box equality is equivalent to False.

theorem helperForTheorem_7_2_dim_eq_zero_of_not_pos {n : ℕ} (hn : ¬0 < n) : n = 0

Helper for Theorem 7.2: a nonpositive ambient dimension must be zero.

theorem boxOuterMeasure_openBox_eq_posDim (n : ℕ) (a b : Fin n → ℝ) (hn : 0 < n) (h : ∀ (i : Fin n), a i ≤ b i) : (boxOuterMeasure n) (Set.Ioo a b) = ENNReal.ofReal (∏ i : Fin n, (b i - a i))

Helper for Theorem 7.2: corrected positive-dimensional form of the open-box outer-measure identity.

theorem boxOuterMeasure_openBox_eq (n : ℕ) (a b : Fin n → ℝ) (hn : 0 < n) (h : ∀ (i : Fin n), a i ≤ b i) : (boxOuterMeasure n) (Set.Ioo a b) = ENNReal.ofReal (∏ i : Fin n, (b i - a i))

Theorem 7.2 (Outer measure of an open box): in positive dimension and under a i ≤ b i, the open box ∏ i, (a i, b i) ⊆ ℝ^n has outer measure ∏ i, (b i - a i).

noncomputable def intervalLength (s : Set ℝ) : ENNReal

Interval length on subsets of ℝ: for sets equal to an open interval (a,b), the value is b - a, and it is +∞ otherwise.

Equations

• intervalLength s = if hIoo : ∃ (p : ℝ × ℝ), s = Set.Ioo p.1 p.2 then have p := Classical.choose hIoo; ENNReal.ofReal (p.2 - p.1) else ⊤

theorem intervalLength_empty : intervalLength ∅ = 0

The interval-length function sends the empty set to zero.

noncomputable def oneDimensionalOuterMeasure : MeasureTheory.OuterMeasure ℝ

The one-dimensional outer measure on ℝ, defined from open-interval length as in the infimum-over-open-covers construction.

Equations

• oneDimensionalOuterMeasure = MeasureTheory.OuterMeasure.ofFunction intervalLength intervalLength_empty

theorem helperForProposition_7_3_volume_le_intervalLength (s : Set ℝ) : MeasureTheory.volume.toOuterMeasure s ≤ intervalLength s

Helper for Proposition 7.3: the outer measure induced by Lebesgue volume on ℝ is pointwise bounded above by intervalLength.

theorem helperForProposition_7_3_volumeOuter_le_oneDimOuter : MeasureTheory.volume.toOuterMeasure ≤ oneDimensionalOuterMeasure

Helper for Proposition 7.3: the outer measure from Lebesgue volume is bounded above by the one-dimensional interval-cover outer measure.

theorem helperForProposition_7_3_volumeOuter_univ : MeasureTheory.volume.toOuterMeasure Set.univ = ⊤

Helper for Proposition 7.3: Lebesgue volume viewed as an outer measure gives infinite mass to ℝ.

theorem proposition_7_3 : oneDimensionalOuterMeasure Set.univ = ⊤

Proposition 7.3: if m* denotes the one-dimensional outer measure on ℝ defined by countable interval covers and interval length, then m*(ℝ) = +∞.

theorem helperForProposition_7_4_intervalLength_Ioo (a b : ℝ) : intervalLength (Set.Ioo a b) = ENNReal.ofReal (b - a)

Helper for Proposition 7.4: intervalLength agrees with Real.volume on open intervals.

theorem helperForProposition_7_4_singleton_outer_le_of_pos (x ε : ℝ) (hε : 0 < ε) : oneDimensionalOuterMeasure {x} ≤ ENNReal.ofReal ε

Helper for Proposition 7.4: each singleton has arbitrarily small one-dimensional outer-measure upper bounds.

theorem helperForProposition_7_4_singleton_outer_eq_zero (x : ℝ) : oneDimensionalOuterMeasure {x} = 0

Helper for Proposition 7.4: every singleton has zero one-dimensional outer measure.

theorem helperForProposition_7_4_countable_outer_eq_zero (A : Set ℝ) (hA : A.Countable) : oneDimensionalOuterMeasure A = 0

Helper for Proposition 7.4: every countable subset of ℝ has zero one-dimensional outer measure.

theorem proposition_7_4 : (∀ (A : Set ℝ), A.Countable → oneDimensionalOuterMeasure A = 0) ∧ oneDimensionalOuterMeasure (Set.range Rat.cast) = 0

Proposition 7.4: if A ⊆ ℝ is countable, then the one-dimensional Lebesgue outer measure satisfies m*(A) = 0. In particular, m*(ℚ) = 0.