theorem helperForProposition_7_12_exists_strictSplitWitness_for_volumeOuterMeasure_of_exists_fixedIcc_strictSplitWitness (hExists : ∃ E ⊆ Set.Icc 0 1, MeasureTheory.volume.toOuterMeasure (Set.Icc 0 1) < MeasureTheory.volume.toOuterMeasure (Set.Icc 0 1 ∩ E) + MeasureTheory.volume.toOuterMeasure (Set.Icc 0 1 \ E)) : ∃ (E : Set ℝ) (T : Set ℝ), MeasureTheory.volume.toOuterMeasure T < MeasureTheory.volume.toOuterMeasure (T ∩ E) + MeasureTheory.volume.toOuterMeasure (T \ E)

Helper for Proposition 7.12: any fixed-interval strict-split witness on Set.Icc (0 : ℝ) 1 is, in particular, a global strict-split witness for Lebesgue outer measure.

theorem helperForProposition_7_12_exists_fixedIcc_strictSplitWitness_for_volumeOuterMeasure_iff_interSimplified : (∃ E ⊆ Set.Icc 0 1, MeasureTheory.volume.toOuterMeasure (Set.Icc 0 1) < MeasureTheory.volume.toOuterMeasure (Set.Icc 0 1 ∩ E) + MeasureTheory.volume.toOuterMeasure (Set.Icc 0 1 \ E)) ↔ ∃ E ⊆ Set.Icc 0 1, MeasureTheory.volume.toOuterMeasure (Set.Icc 0 1) < MeasureTheory.volume.toOuterMeasure E + MeasureTheory.volume.toOuterMeasure (Set.Icc 0 1 \ E)

Helper for Proposition 7.12: for witnesses supported in Set.Icc (0 : ℝ) 1, the term ((Set.Icc (0 : ℝ) 1) ∩ E) simplifies to E in the strict-split inequality.

theorem helperForProposition_7_12_exists_fixedIcc_strictSplitWitness_for_volumeOuterMeasure_of_exists_fullOuterMeasure_IccSubset_with_positiveComplement (hExists : ∃ E ⊆ Set.Icc 0 1, MeasureTheory.volume.toOuterMeasure E = MeasureTheory.volume.toOuterMeasure (Set.Icc 0 1) ∧ 0 < MeasureTheory.volume.toOuterMeasure (Set.Icc 0 1 \ E)) : ∃ E ⊆ Set.Icc 0 1, MeasureTheory.volume.toOuterMeasure (Set.Icc 0 1) < MeasureTheory.volume.toOuterMeasure (Set.Icc 0 1 ∩ E) + MeasureTheory.volume.toOuterMeasure (Set.Icc 0 1 \ E)

Helper for Proposition 7.12: a subset E ⊆ Set.Icc (0 : ℝ) 1 with full outer measure in Set.Icc (0 : ℝ) 1 and positive outer measure complement yields the fixed-interval strict-split witness.

theorem helperForProposition_7_12_exists_nonNullMeasurableSet_volume_Icc_of_isComplete [MeasureTheory.volume.IsComplete] : ∃ E ⊆ Set.Icc 0 1, ¬MeasureTheory.NullMeasurableSet E MeasureTheory.volume

Helper for Proposition 7.12: completeness of Lebesgue measure yields a bounded non-null-measurable witness inside Set.Icc (0 : ℝ) 1.

theorem helperForProposition_7_12_exists_nonNullMeasurableSet_volume_Icc_of_exists_fullOuterMeasure_IccSubset_with_positiveComplement (hExists : ∃ E ⊆ Set.Icc 0 1, MeasureTheory.volume.toOuterMeasure E = MeasureTheory.volume.toOuterMeasure (Set.Icc 0 1) ∧ 0 < MeasureTheory.volume.toOuterMeasure (Set.Icc 0 1 \ E)) : ∃ E ⊆ Set.Icc 0 1, ¬MeasureTheory.NullMeasurableSet E MeasureTheory.volume

Helper for Proposition 7.12: a bounded full-outer-measure witness with positive interval complement already gives a bounded non-null-measurable witness in Set.Icc (0 : ℝ) 1.

theorem helperForProposition_7_12_prereq_exists_nonNullMeasurableSet_volume_Icc : ∃ E ⊆ Set.Icc 0 1, ¬MeasureTheory.NullMeasurableSet E MeasureTheory.volume

Helper for Proposition 7.12: bounded upstream witness in Set.Icc (0 : ℝ) 1 that is not almost-everywhere equal to any measurable set for Lebesgue measure.

theorem helperForProposition_7_12_exists_fixedIcc_strictSplitWitness_for_volumeOuterMeasure_of_exists_nonNullMeasurableSet_volume_Icc (hExists : ∃ E ⊆ Set.Icc 0 1, ¬MeasureTheory.NullMeasurableSet E MeasureTheory.volume) : ∃ E ⊆ Set.Icc 0 1, MeasureTheory.volume.toOuterMeasure (Set.Icc 0 1) < MeasureTheory.volume.toOuterMeasure (Set.Icc 0 1 ∩ E) + MeasureTheory.volume.toOuterMeasure (Set.Icc 0 1 \ E)

Helper for Proposition 7.12: any bounded non-null-measurable witness in Set.Icc (0 : ℝ) 1 yields a fixed-interval strict-split witness for Lebesgue outer measure.

theorem helperForProposition_7_12_exists_fixedIcc_strictSplitWitness_for_volumeOuterMeasure_iff_exists_nonNullMeasurableSet_volume_Icc : (∃ E ⊆ Set.Icc 0 1, MeasureTheory.volume.toOuterMeasure (Set.Icc 0 1) < MeasureTheory.volume.toOuterMeasure (Set.Icc 0 1 ∩ E) + MeasureTheory.volume.toOuterMeasure (Set.Icc 0 1 \ E)) ↔ ∃ E ⊆ Set.Icc 0 1, ¬MeasureTheory.NullMeasurableSet E MeasureTheory.volume

Helper for Proposition 7.12: on Set.Icc (0 : ℝ) 1, fixed-interval strict-split witnesses for Lebesgue outer measure are equivalent to bounded non-null-measurable witnesses.

theorem helperForProposition_7_12_exists_fixedIcc_strictSplitWitness_for_volumeOuterMeasure_iff_exists_nonCaratheodorySet : (∃ E ⊆ Set.Icc 0 1, MeasureTheory.volume.toOuterMeasure (Set.Icc 0 1) < MeasureTheory.volume.toOuterMeasure (Set.Icc 0 1 ∩ E) + MeasureTheory.volume.toOuterMeasure (Set.Icc 0 1 \ E)) ↔ ∃ (E : Set ℝ), ¬MeasureTheory.volume.IsCaratheodory E

Helper for Proposition 7.12: fixed-interval strict-split witnesses on Set.Icc (0 : ℝ) 1 are equivalent to non-Carathéodory witnesses for Lebesgue outer measure on ℝ.

theorem helperForProposition_7_12_exists_IccWitness_notAEEq_any_measurable_of_exists_fixedIcc_strictSplitWitness_for_volumeOuterMeasure (hExists : ∃ E ⊆ Set.Icc 0 1, MeasureTheory.volume.toOuterMeasure (Set.Icc 0 1) < MeasureTheory.volume.toOuterMeasure (Set.Icc 0 1 ∩ E) + MeasureTheory.volume.toOuterMeasure (Set.Icc 0 1 \ E)) : ∃ E ⊆ Set.Icc 0 1, ∀ (t : Set ℝ), MeasurableSet t → ¬E =ᵐ[MeasureTheory.volume] t

Helper for Proposition 7.12: any fixed-interval strict-split witness for Lebesgue outer measure yields a bounded witness in Set.Icc (0 : ℝ) 1 that is not almost-everywhere equal to any measurable set.

theorem helperForProposition_7_12_exists_nonNullMeasurableSet_for_volume_of_exists_fixedIcc_strictSplitWitness_for_volumeOuterMeasure (hExists : ∃ E ⊆ Set.Icc 0 1, MeasureTheory.volume.toOuterMeasure (Set.Icc 0 1) < MeasureTheory.volume.toOuterMeasure (Set.Icc 0 1 ∩ E) + MeasureTheory.volume.toOuterMeasure (Set.Icc 0 1 \ E)) : ∃ (E : Set ℝ), ¬MeasureTheory.NullMeasurableSet E MeasureTheory.volume

Helper for Proposition 7.12: any fixed-interval strict-split witness on Set.Icc (0 : ℝ) 1 yields a global non-null-measurable witness for Lebesgue measure.

theorem prereqForProposition_7_12_exists_set_notAEEq_any_measurableSet_volume_Icc : ∃ E ⊆ Set.Icc 0 1, ∀ (t : Set ℝ), MeasurableSet t → ¬E =ᵐ[MeasureTheory.volume] t

Helper for Proposition 7.12: bounded upstream witness in Set.Icc (0 : ℝ) 1 that is not almost-everywhere equal to any measurable set for Lebesgue measure.

theorem prereqForProposition_7_12_exists_set_notAEEq_any_measurableSet_volume : ∃ (E : Set ℝ), ∀ (t : Set ℝ), MeasurableSet t → ¬E =ᵐ[MeasureTheory.volume] t

Helper for Proposition 7.12: upstream prerequisite witness not almost-everywhere equal to any measurable set for Lebesgue measure.

theorem helperForProposition_7_12_exists_IccWitness_notAEEq_any_measurable_iff_exists_IccWitness_nonNullMeasurable_for_volume : (∃ E ⊆ Set.Icc 0 1, ∀ (t : Set ℝ), MeasurableSet t → ¬E =ᵐ[MeasureTheory.volume] t) ↔ ∃ E ⊆ Set.Icc 0 1, ¬MeasureTheory.NullMeasurableSet E MeasureTheory.volume

Helper for Proposition 7.12: on the bounded interval Set.Icc (0 : ℝ) 1, existence of a witness not almost-everywhere equal to any measurable set is equivalent to existence of a non-null-measurable witness for Lebesgue measure.

theorem helperForProposition_7_12_exists_IccWitness_nonNullMeasurable_for_volume_of_exists_IccWitness_notAEEq (hExists : ∃ E ⊆ Set.Icc 0 1, ∀ (t : Set ℝ), MeasurableSet t → ¬E =ᵐ[MeasureTheory.volume] t) : ∃ E ⊆ Set.Icc 0 1, ¬MeasureTheory.NullMeasurableSet E MeasureTheory.volume

Helper for Proposition 7.12: any bounded witness in Set.Icc (0 : ℝ) 1 that is not almost-everywhere equal to a measurable set is a bounded non-null-measurable witness.

theorem helperForProposition_7_12_exists_IccWitness_notAEEq_any_measurable_for_volume_of_exists_IccWitness_nonNullMeasurable (hExists : ∃ E ⊆ Set.Icc 0 1, ¬MeasureTheory.NullMeasurableSet E MeasureTheory.volume) : ∃ E ⊆ Set.Icc 0 1, ∀ (t : Set ℝ), MeasurableSet t → ¬E =ᵐ[MeasureTheory.volume] t

Helper for Proposition 7.12: any bounded non-null-measurable witness in Set.Icc (0 : ℝ) 1 upgrades to a bounded witness not almost-everywhere equal to any measurable set.

theorem helperForProposition_7_12_exists_set_notAEEq_any_measurableSet_volume_iff_exists_IccWitness_nonNullMeasurable_for_volume : (∃ (E : Set ℝ), ∀ (t : Set ℝ), MeasurableSet t → ¬E =ᵐ[MeasureTheory.volume] t) ↔ ∃ E ⊆ Set.Icc 0 1, ¬MeasureTheory.NullMeasurableSet E MeasureTheory.volume

Helper for Proposition 7.12: a global witness not almost-everywhere equal to any measurable set for Lebesgue measure is equivalent to a bounded non-null-measurable witness in Set.Icc (0 : ℝ) 1.

theorem prereqForProposition_7_12_exists_nonNullMeasurableSet_volume_Icc_direct : ∃ E ⊆ Set.Icc 0 1, ¬MeasureTheory.NullMeasurableSet E MeasureTheory.volume

Helper for Proposition 7.12: direct bounded prerequisite witness in non-null-measurable form for Lebesgue measure.

theorem helperForProposition_7_12_exists_nonCaratheodorySet_of_exists_IccWitness_nonNullMeasurable (hExists : ∃ E ⊆ Set.Icc 0 1, ¬MeasureTheory.NullMeasurableSet E MeasureTheory.volume) : ∃ (E : Set ℝ), ¬MeasureTheory.volume.IsCaratheodory E

Helper for Proposition 7.12: any bounded non-null-measurable witness in Set.Icc (0 : ℝ) 1 yields a non-Carathéodory witness for Lebesgue outer measure.

theorem helperForProposition_7_12_exists_nonNullMeasurableSet_for_volume_of_exists_IccWitness_notAEEq (hExists : ∃ E ⊆ Set.Icc 0 1, ∀ (t : Set ℝ), MeasurableSet t → ¬E =ᵐ[MeasureTheory.volume] t) : ∃ (E : Set ℝ), ¬MeasureTheory.NullMeasurableSet E MeasureTheory.volume

Helper for Proposition 7.12: any bounded witness in Set.Icc (0 : ℝ) 1 that is not almost-everywhere equal to a measurable set yields a non-null-measurable subset of ℝ for Lebesgue measure.

theorem helperForProposition_7_12_exists_nonNullMeasurableSet_for_volume : ∃ (E : Set ℝ), ¬MeasureTheory.NullMeasurableSet E MeasureTheory.volume

Helper for Proposition 7.12: prerequisite existence of a non-null-measurable subset of ℝ for Lebesgue measure.

theorem helperForProposition_7_12_exists_strictSplitWitness_of_exists_nonNullMeasurableSet (hExists : ∃ (E : Set ℝ), ¬MeasureTheory.NullMeasurableSet E MeasureTheory.volume) : ∃ (E : Set ℝ) (T : Set ℝ), MeasureTheory.volume.toOuterMeasure T < MeasureTheory.volume.toOuterMeasure (T ∩ E) + MeasureTheory.volume.toOuterMeasure (T \ E)

Helper for Proposition 7.12: any non-null-measurable witness yields a strict-split witness for Lebesgue outer measure.

theorem helperForProposition_7_12_exists_nonNullMeasurableSet_for_volume_of_exists_strictSplitWitness (hExists : ∃ (E : Set ℝ) (T : Set ℝ), MeasureTheory.volume.toOuterMeasure T < MeasureTheory.volume.toOuterMeasure (T ∩ E) + MeasureTheory.volume.toOuterMeasure (T \ E)) : ∃ (E : Set ℝ), ¬MeasureTheory.NullMeasurableSet E MeasureTheory.volume

Helper for Proposition 7.12: any strict-split witness for Lebesgue outer measure yields a non-null-measurable subset of ℝ.

theorem helperForProposition_7_12_exists_strictSplitWitness_for_volumeOuterMeasure_iff_exists_nonNullMeasurableSet_for_volume : (∃ (E : Set ℝ) (T : Set ℝ), MeasureTheory.volume.toOuterMeasure T < MeasureTheory.volume.toOuterMeasure (T ∩ E) + MeasureTheory.volume.toOuterMeasure (T \ E)) ↔ ∃ (E : Set ℝ), ¬MeasureTheory.NullMeasurableSet E MeasureTheory.volume

Helper for Proposition 7.12: for Lebesgue outer measure on ℝ, strict-split witnesses exist if and only if non-null-measurable sets exist for Lebesgue measure.

theorem helperForProposition_7_12_exists_strictSplitWitness_for_volumeOuterMeasure_of_exists_IccWitness_notAEEq (hExists : ∃ E ⊆ Set.Icc 0 1, ∀ (t : Set ℝ), MeasurableSet t → ¬E =ᵐ[MeasureTheory.volume] t) : ∃ (E : Set ℝ) (T : Set ℝ), MeasureTheory.volume.toOuterMeasure T < MeasureTheory.volume.toOuterMeasure (T ∩ E) + MeasureTheory.volume.toOuterMeasure (T \ E)

Helper for Proposition 7.12: any bounded witness in Set.Icc (0 : ℝ) 1 that is not almost-everywhere equal to a measurable set yields a strict-split witness for Lebesgue outer measure.

theorem helperForProposition_7_12_exists_strictSplitWitness_for_volumeOuterMeasure : ∃ (E : Set ℝ) (T : Set ℝ), MeasureTheory.volume.toOuterMeasure T < MeasureTheory.volume.toOuterMeasure (T ∩ E) + MeasureTheory.volume.toOuterMeasure (T \ E)

Helper for Proposition 7.12: prerequisite strict-split witness for Lebesgue outer measure on ℝ.

theorem helperForProposition_7_12_exists_nonCaratheodorySet_of_exists_IccWitness_notAEEq (hExists : ∃ E ⊆ Set.Icc 0 1, ∀ (t : Set ℝ), MeasurableSet t → ¬E =ᵐ[MeasureTheory.volume] t) : ∃ (E : Set ℝ), ¬MeasureTheory.volume.IsCaratheodory E

Helper for Proposition 7.12: any bounded witness in Set.Icc (0 : ℝ) 1 that is not almost-everywhere equal to any measurable set yields a non-Carathéodory witness for Lebesgue outer measure.

theorem helperForProposition_7_12_exists_nonCaratheodorySet : ∃ (E : Set ℝ), ¬MeasureTheory.volume.IsCaratheodory E

Proposition 7.12 helper: there exists a subset of ℝ that is not Carathéodory measurable for Lebesgue outer measure.

theorem helperForProposition_7_12_exists_strictSplit {m : MeasureTheory.OuterMeasure ℝ} {E : Set ℝ} (hE : ¬m.IsCaratheodory E) : ∃ (T : Set ℝ), m T < m (T ∩ E) + m (T \ E)

Helper for Proposition 7.12: non-Carathéodory measurability yields a strict split inequality.

theorem helperForProposition_7_12_exists_strictSplit_for_volumeOuterMeasure : ∃ (E : Set ℝ) (T : Set ℝ), MeasureTheory.volume.toOuterMeasure T < MeasureTheory.volume.toOuterMeasure (T ∩ E) + MeasureTheory.volume.toOuterMeasure (T \ E)

Helper for Proposition 7.12: a strict-split witness for Lebesgue outer measure follows from the non-Carathéodory witness.

theorem helperForProposition_7_12_strictSplit_implies_nonCaratheodory {m : MeasureTheory.OuterMeasure ℝ} {E T : Set ℝ} (hStrict : m T < m (T ∩ E) + m (T \ E)) : ¬m.IsCaratheodory E

Helper for Proposition 7.12: any strict split inequality certifies that the set is not Carathéodory measurable for the outer measure.

theorem helperForProposition_7_12_nonCaratheodory_iff_exists_strictSplit {m : MeasureTheory.OuterMeasure ℝ} {E : Set ℝ} : ¬m.IsCaratheodory E ↔ ∃ (T : Set ℝ), m T < m (T ∩ E) + m (T \ E)

Helper for Proposition 7.12: non-Carathéodory measurability is equivalent to the existence of a strict split inequality witness.

theorem helperForProposition_7_12_pairwiseDisjointFamilyFromTwoPieces (E T : Set ℝ) : (Pairwise fun (i j : ℕ) => Disjoint (helperForProposition_7_12_twoPieceFamily E T i) (helperForProposition_7_12_twoPieceFamily E T j)) ∧ ⋃ (n : ℕ), helperForProposition_7_12_twoPieceFamily E T n = T

Helper for Proposition 7.12: the two-piece family is pairwise disjoint and unions back to T.

theorem helperForProposition_7_12_tsumFamilyFromTwoPieces (m : MeasureTheory.OuterMeasure ℝ) (E T : Set ℝ) : ∑' (n : ℕ), m (helperForProposition_7_12_twoPieceFamily E T n) = m (T ∩ E) + m (T \ E)

Helper for Proposition 7.12: the outer-measure sum of the two-piece family is the two-term sum.

theorem helperForProposition_7_12_notEq_from_strictSplit (m : MeasureTheory.OuterMeasure ℝ) (E T : Set ℝ) (hStrict : m T < m (T ∩ E) + m (T \ E)) : m (⋃ (n : ℕ), helperForProposition_7_12_twoPieceFamily E T n) ≠ ∑' (n : ℕ), m (helperForProposition_7_12_twoPieceFamily E T n)

Helper for Proposition 7.12: strict two-piece inequality implies failure of countable additivity for the associated countable family.

theorem helperForProposition_7_12_nonNullMeasurable_of_strictSplitWitness_for_volumeOuterMeasure {E T : Set ℝ} (hStrict : MeasureTheory.volume.toOuterMeasure T < MeasureTheory.volume.toOuterMeasure (T ∩ E) + MeasureTheory.volume.toOuterMeasure (T \ E)) : ¬MeasureTheory.NullMeasurableSet E MeasureTheory.volume

Helper for Proposition 7.12: any strict split witness for Lebesgue outer measure gives a non-null-measurable subset of ℝ.

theorem helperForProposition_7_12_exists_IccStrictSplitWitness_for_volumeOuterMeasure_of_exists_IccWitness_notAEEq (hExists : ∃ E ⊆ Set.Icc 0 1, ∀ (t : Set ℝ), MeasurableSet t → ¬E =ᵐ[MeasureTheory.volume] t) : ∃ (E : Set ℝ) (T : Set ℝ), E ⊆ Set.Icc 0 1 ∧ MeasureTheory.volume.toOuterMeasure T < MeasureTheory.volume.toOuterMeasure (T ∩ E) + MeasureTheory.volume.toOuterMeasure (T \ E)

Helper for Proposition 7.12: a bounded witness in Set.Icc (0 : ℝ) 1 that is not almost-everywhere equal to any measurable set yields a bounded strict-split witness for Lebesgue outer measure with the same split set.

theorem helperForProposition_7_12_exists_IccWitness_notAEEq_of_exists_IccStrictSplitWitness_for_volumeOuterMeasure (hExists : ∃ (E : Set ℝ) (T : Set ℝ), E ⊆ Set.Icc 0 1 ∧ MeasureTheory.volume.toOuterMeasure T < MeasureTheory.volume.toOuterMeasure (T ∩ E) + MeasureTheory.volume.toOuterMeasure (T \ E)) : ∃ E ⊆ Set.Icc 0 1, ∀ (t : Set ℝ), MeasurableSet t → ¬E =ᵐ[MeasureTheory.volume] t

Helper for Proposition 7.12: a bounded strict-split witness whose split set lies in Set.Icc (0 : ℝ) 1 yields a bounded witness not almost-everywhere equal to any measurable set.

theorem helperForProposition_7_12_exists_IccWitness_notAEEq_iff_exists_IccStrictSplitWitness_for_volumeOuterMeasure : (∃ E ⊆ Set.Icc 0 1, ∀ (t : Set ℝ), MeasurableSet t → ¬E =ᵐ[MeasureTheory.volume] t) ↔ ∃ (E : Set ℝ) (T : Set ℝ), E ⊆ Set.Icc 0 1 ∧ MeasureTheory.volume.toOuterMeasure T < MeasureTheory.volume.toOuterMeasure (T ∩ E) + MeasureTheory.volume.toOuterMeasure (T \ E)

Helper for Proposition 7.12: bounded not-a.e.-equal witnesses in Set.Icc (0 : ℝ) 1 are equivalent to bounded strict-split witnesses for Lebesgue outer measure with split set in the same interval.

theorem helperForProposition_7_12_exists_nonNullMeasurableSet_of_exists_strictSplitWitness_volume_Icc (hExists : ∃ (E : Set ℝ), ∃ T ⊆ Set.Icc 0 1, MeasureTheory.volume.toOuterMeasure T < MeasureTheory.volume.toOuterMeasure (T ∩ E) + MeasureTheory.volume.toOuterMeasure (T \ E)) : ∃ (E : Set ℝ), ¬MeasureTheory.NullMeasurableSet E MeasureTheory.volume

Helper for Proposition 7.12: a bounded strict-split witness on Set.Icc (0 : ℝ) 1 already produces a non-null-measurable subset of ℝ for Lebesgue measure.

theorem helperForProposition_7_12_exists_family_of_exists_strictSplitWitness_for_volumeOuterMeasure (hExists : ∃ (E : Set ℝ) (T : Set ℝ), MeasureTheory.volume.toOuterMeasure T < MeasureTheory.volume.toOuterMeasure (T ∩ E) + MeasureTheory.volume.toOuterMeasure (T \ E)) : ∃ (A : ℕ → Set ℝ), (Pairwise fun (i j : ℕ) => Disjoint (A i) (A j)) ∧ MeasureTheory.volume.toOuterMeasure (⋃ (j : ℕ), A j) ≠ ∑' (j : ℕ), MeasureTheory.volume.toOuterMeasure (A j)

Helper for Proposition 7.12: any strict split witness for Lebesgue outer measure directly yields a countable pairwise-disjoint family on which outer measure fails countable additivity.

theorem proposition_7_12 : ∃ (A : ℕ → Set ℝ), (Pairwise fun (i j : ℕ) => Disjoint (A i) (A j)) ∧ MeasureTheory.volume.toOuterMeasure (⋃ (j : ℕ), A j) ≠ ∑' (j : ℕ), MeasureTheory.volume.toOuterMeasure (A j)

Proposition 7.12 (Failure of countable additivity): there exists a countably infinite family (A_j)_{j∈ℕ} of pairwise disjoint subsets of ℝ such that Lebesgue outer measure on ℝ is not countably additive on this family: m*(⋃ j, A_j) ≠ ∑' j, m*(A_j).

def helperForProposition_7_13_twoPieceFamilyFin (E T : Set ℝ) : Fin 2 → Set ℝ

Helper for Proposition 7.13: the finite two-piece family indexed by Fin 2, with 0 ↦ T ∩ E and 1 ↦ T \ E.

Equations

• helperForProposition_7_13_twoPieceFamilyFin E T i = if ↑i = 0 then T ∩ E else T \ E

theorem helperForProposition_7_13_pairwiseDisjoint_twoPieceFamilyFin (E T : Set ℝ) : Pairwise fun (i j : Fin 2) => Disjoint (helperForProposition_7_13_twoPieceFamilyFin E T i) (helperForProposition_7_13_twoPieceFamilyFin E T j)

Helper for Proposition 7.13: the two-piece Fin 2 family is pairwise disjoint.

theorem helperForProposition_7_13_union_and_sum_twoPieceFamilyFin (m : MeasureTheory.OuterMeasure ℝ) (E T : Set ℝ) : m (⋃ (j : Fin 2), helperForProposition_7_13_twoPieceFamilyFin E T j) = m T ∧ ∑ j : Fin 2, m (helperForProposition_7_13_twoPieceFamilyFin E T j) = m (T ∩ E) + m (T \ E)

Helper for Proposition 7.13: for the two-piece Fin 2 family, the union has measure m T and the finite sum is m (T ∩ E) + m (T \ E).

theorem helperForProposition_7_13_notEq_from_strictSplit_fin (m : MeasureTheory.OuterMeasure ℝ) (E T : Set ℝ) (hStrict : m T < m (T ∩ E) + m (T \ E)) : m (⋃ (j : Fin 2), helperForProposition_7_13_twoPieceFamilyFin E T j) ≠ ∑ j : Fin 2, m (helperForProposition_7_13_twoPieceFamilyFin E T j)

Helper for Proposition 7.13: a strict split inequality forces failure of finite additivity for the associated two-piece Fin 2 family.

theorem proposition_7_13 : ∃ (n : ℕ) (A : Fin n → Set ℝ), (Pairwise fun (i j : Fin n) => Disjoint (A i) (A j)) ∧ MeasureTheory.volume.toOuterMeasure (⋃ (j : Fin n), A j) ≠ ∑ j : Fin n, MeasureTheory.volume.toOuterMeasure (A j)

Proposition 7.13 (Failure of finite additivity): there exists a finite family (A_j)_{j∈J} of pairwise disjoint subsets of ℝ such that Lebesgue outer measure on ℝ is not finitely additive on this family: m*(⋃ j, A_j) ≠ ∑ j, m*(A_j).