Measure Theory and Integration

2.6. Failure of Additivity🔗

We show that there exist a pair of sets that do not satisfy additivity.

As preparation, we first recall the translation invariance of measure.

Lemma (Translation Invariance).

For every set A \subseteq \mathbb{R} and every c \in \mathbb{R}, m(\{x \mid x - c \in A\}) = m(A).

Lean code
def translate (A : Set ℝ) (c : ℝ) : Set ℝ := {x | x - c ∈ A}
theorem measure_translate_le (A : Set ℝ) (c : ℝ) : measure (translate A c) ≤ measure A := A:Set ℝc:ℝ⊢ measure (translate A c) ≤ measure A A:Set ℝc:ℝa:ℕ → ℝb:ℕ → ℝhA:A ⊆ ⋃ i, Ioo (a i) (b i)⊢ measure (translate A c) ≤ ∑' (i : ℕ), ENNReal.ofReal (b i - a i) have hA' : translate A c ⊆ ⋃ n, Ioo (a n + c) (b n + c) := A:Set ℝc:ℝ⊢ measure (translate A c) ≤ measure A intro x A:Set ℝc:ℝa:ℕ → ℝb:ℕ → ℝhA:A ⊆ ⋃ i, Ioo (a i) (b i)x:ℝhx:x ∈ translate A c⊢ x ∈ ⋃ n, Ioo (a n + c) (b n + c) A:Set ℝc:ℝa:ℕ → ℝb:ℕ → ℝhA:A ⊆ ⋃ i, Ioo (a i) (b i)x:ℝhx:x ∈ translate A cn:ℕhn:x - c ∈ Ioo (a n) (b n)⊢ x ∈ ⋃ n, Ioo (a n + c) (b n + c) A:Set ℝc:ℝa:ℕ → ℝb:ℕ → ℝhA:A ⊆ ⋃ i, Ioo (a i) (b i)x:ℝhx:x ∈ translate A cn:ℕhn:x - c ∈ Ioo (a n) (b n)⊢ x ∈ Ioo (a n + c) (b n + c) A:Set ℝc:ℝa:ℕ → ℝb:ℕ → ℝhA:A ⊆ ⋃ i, Ioo (a i) (b i)x:ℝhx:x ∈ translate A cn:ℕhna:a n < x - chnb:x - c < b n⊢ x ∈ Ioo (a n + c) (b n + c) A:Set ℝc:ℝa:ℕ → ℝb:ℕ → ℝhA:A ⊆ ⋃ i, Ioo (a i) (b i)x:ℝhx:x ∈ translate A cn:ℕhna:a n < x - chnb:x - c < b n⊢ a n + c < xA:Set ℝc:ℝa:ℕ → ℝb:ℕ → ℝhA:A ⊆ ⋃ i, Ioo (a i) (b i)x:ℝhx:x ∈ translate A cn:ℕhna:a n < x - chnb:x - c < b n⊢ x < b n + c A:Set ℝc:ℝa:ℕ → ℝb:ℕ → ℝhA:A ⊆ ⋃ i, Ioo (a i) (b i)x:ℝhx:x ∈ translate A cn:ℕhna:a n < x - chnb:x - c < b n⊢ a n + c < xA:Set ℝc:ℝa:ℕ → ℝb:ℕ → ℝhA:A ⊆ ⋃ i, Ioo (a i) (b i)x:ℝhx:x ∈ translate A cn:ℕhna:a n < x - chnb:x - c < b n⊢ x < b n + c All goals completed! 🐙 calc measure (translate A c) ≤ ∑' n, ENNReal.ofReal ((b n + c) - (a n + c)) := measure_le _ _ _ hA' _ = ∑' n, ENNReal.ofReal (b n - a n) := A:Set ℝc:ℝa:ℕ → ℝb:ℕ → ℝhA:A ⊆ ⋃ i, Ioo (a i) (b i)hA':translate A c ⊆ ⋃ n, Ioo (a n + c) (b n + c) := fun ⦃x⦄ hx => Exists.casesOn (mem_iUnion.mp (hA hx)) fun n hn => mem_iUnion.mpr (Exists.intro n (And.casesOn hn fun hna hnb => ⟨measure_translate_le._proof_1 c a n hna, measure_translate_le._proof_2 c b n hnb⟩))⊢ ∑' (n : ℕ), ENNReal.ofReal (b n + c - (a n + c)) = ∑' (n : ℕ), ENNReal.ofReal (b n - a n) All goals completed! 🐙
theorem measure_translate (A : Set ℝ) (c : ℝ) : measure (translate A c) = measure A := A:Set ℝc:ℝ⊢ measure (translate A c) = measure A A:Set ℝc:ℝ⊢ measure A ≤ measure (translate A c) All goals completed! 🐙
Definition (Vitali Set).

A set A \subseteq \mathbb{R} is called a Vitali set if A \subseteq [0,1] and, for every x \in \mathbb{R} there exists a unique rational number q such that x - q \in A.

Lean code
structure IsVitali (A : Set ℝ) : Prop where exists_rational : ∀ x : ℝ, ∃! q : ℚ, x - q ∈ A subset_Icc_zero_one : A ⊆ Icc 0 1
Lemma.

If A is a Vitali set, then m(A) \neq 0.

Lean code
theorem IsVitali.Icc_zero_one_subset_iUnion_translate {A : Set ℝ} (hA : IsVitali A) : Icc 0 1 ⊆ ⋃ q : (Icc (-1) 1 : Set ℚ), translate A (q : ℚ) := A:Set ℝhA:IsVitali A⊢ Icc 0 1 ⊆ ⋃ q, translate A ↑↑q intro x A:Set ℝhA:IsVitali Ax:ℝhx:x ∈ Icc 0 1⊢ x ∈ ⋃ q, translate A ↑↑q A:Set ℝhA:IsVitali Ax:ℝhx:x ∈ Icc 0 1q:ℚhqA:x - ↑q ∈ Aright✝:∀ (y : ℚ), (fun q => x - ↑q ∈ A) y → y = q⊢ x ∈ ⋃ q, translate A ↑↑q have hq_lower : (-1 : ℚ) ≤ q := A:Set ℝhA:IsVitali A⊢ Icc 0 1 ⊆ ⋃ q, translate A ↑↑q suffices (q : ℝ) ≥ -1 A:Set ℝhA:IsVitali Ax:ℝhx:x ∈ Icc 0 1q:ℚhqA:x - ↑q ∈ Aright✝:∀ (y : ℚ), (fun q => x - ↑q ∈ A) y → y = qthis:↑q ≥ -1 := ?m.58⊢ -1 ≤ q All goals completed! 🐙 A:Set ℝhA:IsVitali Ax:ℝhx:x ∈ Icc 0 1q:ℚhqA:x - ↑q ∈ Aright✝:∀ (y : ℚ), (fun q => x - ↑q ∈ A) y → y = qhxq:x - ↑q ∈ Icc 0 1 := hA.subset_Icc_zero_one hqA⊢ ↑q ≥ -1 All goals completed! 🐙 have hq_upper : q ≤ (1 : ℚ) := A:Set ℝhA:IsVitali A⊢ Icc 0 1 ⊆ ⋃ q, translate A ↑↑q suffices (q : ℝ) ≤ 1 A:Set ℝhA:IsVitali Ax:ℝhx:x ∈ Icc 0 1q:ℚhqA:x - ↑q ∈ Aright✝:∀ (y : ℚ), (fun q => x - ↑q ∈ A) y → y = qhq_lower:-1 ≤ q := have this := have hxq := hA.subset_Icc_zero_one hqA; Icc_zero_one_subset_iUnion_translate._proof_1 hx q hxq; cast (Eq.trans (Eq.trans (congrArg (GE.ge ↑q) (congrArg Neg.neg (Eq.symm Nat.cast_one))) (Eq.trans (congrArg (GE.ge ↑q) (Int.cast_negSucc._simp_1 0)) Rat.intCast_le_cast._simp_1)) (Eq.symm (Eq.trans (congrFun' (congrArg LE.le (congrArg Neg.neg (Eq.symm Nat.cast_one))) q) (congrFun' (congrArg LE.le (Int.cast_negSucc._simp_1 0)) q)))) thisthis:↑q ≤ 1 := ?m.91⊢ q ≤ 1 All goals completed! 🐙 A:Set ℝhA:IsVitali Ax:ℝhx:x ∈ Icc 0 1q:ℚhqA:x - ↑q ∈ Aright✝:∀ (y : ℚ), (fun q => x - ↑q ∈ A) y → y = qhq_lower:-1 ≤ q := have this := have hxq := hA.subset_Icc_zero_one hqA; Icc_zero_one_subset_iUnion_translate._proof_1 hx q hxq; cast (Eq.trans (Eq.trans (congrArg (GE.ge ↑q) (congrArg Neg.neg (Eq.symm Nat.cast_one))) (Eq.trans (congrArg (GE.ge ↑q) (Int.cast_negSucc._simp_1 0)) Rat.intCast_le_cast._simp_1)) (Eq.symm (Eq.trans (congrFun' (congrArg LE.le (congrArg Neg.neg (Eq.symm Nat.cast_one))) q) (congrFun' (congrArg LE.le (Int.cast_negSucc._simp_1 0)) q)))) thishxq:x - ↑q ∈ Icc 0 1 := hA.subset_Icc_zero_one hqA⊢ ↑q ≤ 1 All goals completed! 🐙 A:Set ℝhA:IsVitali Ax:ℝhx:x ∈ Icc 0 1q:ℚhqA:x - ↑q ∈ Aright✝:∀ (y : ℚ), (fun q => x - ↑q ∈ A) y → y = qhq_lower:-1 ≤ q := have this := have hxq := hA.subset_Icc_zero_one hqA; Icc_zero_one_subset_iUnion_translate._proof_1 hx q hxq; cast (Eq.trans (Eq.trans (congrArg (GE.ge ↑q) (congrArg Neg.neg (Eq.symm Nat.cast_one))) (Eq.trans (congrArg (GE.ge ↑q) (Int.cast_negSucc._simp_1 0)) Rat.intCast_le_cast._simp_1)) (Eq.symm (Eq.trans (congrFun' (congrArg LE.le (congrArg Neg.neg (Eq.symm Nat.cast_one))) q) (congrFun' (congrArg LE.le (Int.cast_negSucc._simp_1 0)) q)))) thishq_upper:q ≤ 1 := have this := have hxq := hA.subset_Icc_zero_one hqA; Icc_zero_one_subset_iUnion_translate._proof_2 hx q hxq; cast (Eq.trans (Eq.trans (Eq.trans (congrArg (LE.le ↑q) (Eq.symm Nat.cast_one)) Rat.cast_le_natCast._simp_1) (congrArg (LE.le q) Nat.cast_one)) (Eq.symm (Eq.trans (congrArg (LE.le q) (Eq.symm Nat.cast_one)) (congrArg (LE.le q) Nat.cast_one)))) this⊢ x ∈ translate A ↑↑⟨q, ⋯⟩ All goals completed! 🐙
theorem IsVitali.measure_ne_zero {A : Set ℝ} (hA : IsVitali A) : measure A ≠ 0 := A:Set ℝhA:IsVitali A⊢ measure A ≠ 0 A:Set ℝhA:IsVitali Ahzero:measure A = 0⊢ False suffices hcontra : (1 : ℝ≥0∞) ≤ 0 A:Set ℝhA:IsVitali Ahzero:measure A = 0hcontra:1 ≤ 0 := ?m.16⊢ False All goals completed! 🐙 calc (1 : ℝ≥0∞) = measure (Icc 0 1) := measure_Icc_zero_one.symm _ ≤ measure (⋃ q : (Icc (-1) 1 : Set ℚ), translate A (q : ℚ)) := A:Set ℝhA:IsVitali Ahzero:measure A = 0⊢ measure (Icc 0 1) ≤ measure (⋃ q, translate A ↑↑q) All goals completed! 🐙 _ ≤ ∑' q : (Icc (-1) 1 : Set ℚ), measure (translate A (q : ℚ)) := measure_iUnion_le_countable _ _ = 0 := A:Set ℝhA:IsVitali Ahzero:measure A = 0⊢ ∑' (q : ↑(Icc (-1) 1)), measure (translate A ↑↑q) = 0 All goals completed! 🐙
Lemma.

If A is a Vitali set and E \subseteq A is measurable, then m(E) = 0.

Lean code
theorem IsVitali.measure_eq_zero_of_measurableSet_subset {A E : Set ℝ} (hA : IsVitali A) (hE : MeasurableSet E) (hEA : E ⊆ A) : measure E = 0 := A:Set ℝE:Set ℝhA:IsVitali AhE:MeasurableSet EhEA:E ⊆ A⊢ measure E = 0 A:Set ℝE:Set ℝhA:IsVitali AhE:MeasurableSet EhEA:E ⊆ Aι:Set ℚ := Ioc 0 1⊢ measure E = 0 A:Set ℝE:Set ℝhA:IsVitali AhE:MeasurableSet EhEA:E ⊆ Aι:Set ℚ := Ioc 0 1B:↑ι → Set ℝ := fun q => translate E ↑↑q⊢ measure E = 0 have hBdisj : Pairwise (Disjoint on B) := A:Set ℝE:Set ℝhA:IsVitali AhE:MeasurableSet EhEA:E ⊆ A⊢ measure E = 0 intro q A:Set ℝE:Set ℝhA:IsVitali AhE:MeasurableSet EhEA:E ⊆ Aι:Set ℚ := Ioc 0 1B:↑ι → Set ℝ := fun q => translate E ↑↑qq:↑ιr:↑ι⊢ q ≠ r → (Disjoint on B) q r A:Set ℝE:Set ℝhA:IsVitali AhE:MeasurableSet EhEA:E ⊆ Aι:Set ℚ := Ioc 0 1B:↑ι → Set ℝ := fun q => translate E ↑↑qq:↑ιr:↑ιhqr:q ≠ r⊢ (Disjoint on B) q r A:Set ℝE:Set ℝhA:IsVitali AhE:MeasurableSet EhEA:E ⊆ Aι:Set ℚ := Ioc 0 1B:↑ι → Set ℝ := fun q => translate E ↑↑qq:↑ιr:↑ιhqr:q ≠ r⊢ B q ∩ B r = ∅ All goals completed! 🐙 have hBsub : ⋃ q, B q ⊆ Icc 0 2 := A:Set ℝE:Set ℝhA:IsVitali AhE:MeasurableSet EhEA:E ⊆ A⊢ measure E = 0 intro x A:Set ℝE:Set ℝhA:IsVitali AhE:MeasurableSet EhEA:E ⊆ Aι:Set ℚ := Ioc 0 1B:↑ι → Set ℝ := fun q => translate E ↑↑qhBdisj:Pairwise (Disjoint on B) := fun ⦃q r⦄ hqr => have this := disjoint_translate_of_subset hA hEA fun h => hqr (Subtype.ext h); disjoint_iff_inter_eq_empty.mpr thisx:ℝhx:x ∈ ⋃ q, B q⊢ x ∈ Icc 0 2 A:Set ℝE:Set ℝhA:IsVitali AhE:MeasurableSet EhEA:E ⊆ Aι:Set ℚ := Ioc 0 1B:↑ι → Set ℝ := fun q => translate E ↑↑qhBdisj:Pairwise (Disjoint on B) := fun ⦃q r⦄ hqr => have this := disjoint_translate_of_subset hA hEA fun h => hqr (Subtype.ext h); disjoint_iff_inter_eq_empty.mpr thisx:ℝhx:x ∈ ⋃ q, B qq:↑ιhq:x ∈ B q⊢ x ∈ Icc 0 2 exact translate_subset_Icc_zero_two (hEA.trans hA.subset_Icc_zero_one) (q : ℝ) (A:Set ℝE:Set ℝhA:IsVitali AhE:MeasurableSet EhEA:E ⊆ Aι:Set ℚ := Ioc 0 1B:↑ι → Set ℝ := fun q => translate E ↑↑qhBdisj:Pairwise (Disjoint on B) := fun ⦃q r⦄ hqr => have this := disjoint_translate_of_subset hA hEA fun h => hqr (Subtype.ext h); disjoint_iff_inter_eq_empty.mpr thisx:ℝhx:x ∈ ⋃ q, B qq:↑ιhq:x ∈ B q⊢ 0 ≤ ↑↑q All goals completed! 🐙) (A:Set ℝE:Set ℝhA:IsVitali AhE:MeasurableSet EhEA:E ⊆ Aι:Set ℚ := Ioc 0 1B:↑ι → Set ℝ := fun q => translate E ↑↑qhBdisj:Pairwise (Disjoint on B) := fun ⦃q r⦄ hqr => have this := disjoint_translate_of_subset hA hEA fun h => hqr (Subtype.ext h); disjoint_iff_inter_eq_empty.mpr thisx:ℝhx:x ∈ ⋃ q, B qq:↑ιhq:x ∈ B q⊢ ↑↑q ≤ 1 All goals completed! 🐙) (A:Set ℝE:Set ℝhA:IsVitali AhE:MeasurableSet EhEA:E ⊆ Aι:Set ℚ := Ioc 0 1B:↑ι → Set ℝ := fun q => translate E ↑↑qhBdisj:Pairwise (Disjoint on B) := fun ⦃q r⦄ hqr => have this := disjoint_translate_of_subset hA hEA fun h => hqr (Subtype.ext h); disjoint_iff_inter_eq_empty.mpr thisx:ℝhx:x ∈ ⋃ q, B qq:↑ιhq:x ∈ B q⊢ x ∈ translate E ↑↑q All goals completed! 🐙) A:Set ℝE:Set ℝhA:IsVitali AhE:MeasurableSet EhEA:E ⊆ Aι:Set ℚ := Ioc 0 1B:↑ι → Set ℝ := fun q => translate E ↑↑qhBdisj:Pairwise (Disjoint on B) := fun ⦃q r⦄ hqr => have this := disjoint_translate_of_subset hA hEA fun h => hqr (Subtype.ext h); disjoint_iff_inter_eq_empty.mpr thishBsub:⋃ q, B q ⊆ Icc 0 2 := fun ⦃x⦄ hx => Exists.casesOn (mem_iUnion.mp hx) fun q hq => translate_subset_Icc_zero_two (HasSubset.Subset.trans hEA hA.subset_Icc_zero_one) (↑↑q) (cast (Eq.trans (Eq.trans (congrFun' (congrArg LE.le (Eq.symm Nat.cast_zero)) ↑q) (congrFun' (congrArg LE.le Nat.cast_zero) ↑q)) (Eq.symm (Eq.trans (Eq.trans (congrFun' (congrArg LE.le (Eq.symm Nat.cast_zero)) ↑↑q) Rat.natCast_le_cast._simp_1) (congrFun' (congrArg LE.le Nat.cast_zero) ↑q)))) (le_of_lt q.property.left)) (cast (Eq.trans (Eq.trans (congrArg (LE.le ↑q) (Eq.symm Nat.cast_one)) (congrArg (LE.le ↑q) Nat.cast_one)) (Eq.symm (Eq.trans (Eq.trans (congrArg (LE.le ↑↑q) (Eq.symm Nat.cast_one)) Rat.cast_le_natCast._simp_1) (congrArg (LE.le ↑q) Nat.cast_one)))) q.property.right) (Eq.mpr (id mem_translate._simp_1) (Eq.mp mem_translate._simp_1 hq))hE0:¬measure E = 0⊢ False suffices hcontra : (∞ : ℝ≥0∞) ≤ 2 A:Set ℝE:Set ℝhA:IsVitali AhE:MeasurableSet EhEA:E ⊆ Aι:Set ℚ := Ioc 0 1B:↑ι → Set ℝ := fun q => translate E ↑↑qhBdisj:Pairwise (Disjoint on B) := fun ⦃q r⦄ hqr => have this := disjoint_translate_of_subset hA hEA fun h => hqr (Subtype.ext h); disjoint_iff_inter_eq_empty.mpr thishBsub:⋃ q, B q ⊆ Icc 0 2 := fun ⦃x⦄ hx => Exists.casesOn (mem_iUnion.mp hx) fun q hq => translate_subset_Icc_zero_two (HasSubset.Subset.trans hEA hA.subset_Icc_zero_one) (↑↑q) (cast (Eq.trans (Eq.trans (congrFun' (congrArg LE.le (Eq.symm Nat.cast_zero)) ↑q) (congrFun' (congrArg LE.le Nat.cast_zero) ↑q)) (Eq.symm (Eq.trans (Eq.trans (congrFun' (congrArg LE.le (Eq.symm Nat.cast_zero)) ↑↑q) Rat.natCast_le_cast._simp_1) (congrFun' (congrArg LE.le Nat.cast_zero) ↑q)))) (le_of_lt q.property.left)) (cast (Eq.trans (Eq.trans (congrArg (LE.le ↑q) (Eq.symm Nat.cast_one)) (congrArg (LE.le ↑q) Nat.cast_one)) (Eq.symm (Eq.trans (Eq.trans (congrArg (LE.le ↑↑q) (Eq.symm Nat.cast_one)) Rat.cast_le_natCast._simp_1) (congrArg (LE.le ↑q) Nat.cast_one)))) q.property.right) (Eq.mpr (id mem_translate._simp_1) (Eq.mp mem_translate._simp_1 hq))hE0:¬measure E = 0hcontra:∞ ≤ 2 := ?m.136⊢ False All goals completed! 🐙 calc ∞ = ∑' _ : ι, measure E := (ENNReal.tsum_const_eq_top_of_ne_zero hE0).symm _ = ∑' q : ι, measure (B q) := A:Set ℝE:Set ℝhA:IsVitali AhE:MeasurableSet EhEA:E ⊆ Aι:Set ℚ := Ioc 0 1B:↑ι → Set ℝ := fun q => translate E ↑↑qhBdisj:Pairwise (Disjoint on B) := fun ⦃q r⦄ hqr => have this := disjoint_translate_of_subset hA hEA fun h => hqr (Subtype.ext h); disjoint_iff_inter_eq_empty.mpr thishBsub:⋃ q, B q ⊆ Icc 0 2 := fun ⦃x⦄ hx => Exists.casesOn (mem_iUnion.mp hx) fun q hq => translate_subset_Icc_zero_two (HasSubset.Subset.trans hEA hA.subset_Icc_zero_one) (↑↑q) (cast (Eq.trans (Eq.trans (congrFun' (congrArg LE.le (Eq.symm Nat.cast_zero)) ↑q) (congrFun' (congrArg LE.le Nat.cast_zero) ↑q)) (Eq.symm (Eq.trans (Eq.trans (congrFun' (congrArg LE.le (Eq.symm Nat.cast_zero)) ↑↑q) Rat.natCast_le_cast._simp_1) (congrFun' (congrArg LE.le Nat.cast_zero) ↑q)))) (le_of_lt q.property.left)) (cast (Eq.trans (Eq.trans (congrArg (LE.le ↑q) (Eq.symm Nat.cast_one)) (congrArg (LE.le ↑q) Nat.cast_one)) (Eq.symm (Eq.trans (Eq.trans (congrArg (LE.le ↑↑q) (Eq.symm Nat.cast_one)) Rat.cast_le_natCast._simp_1) (congrArg (LE.le ↑q) Nat.cast_one)))) q.property.right) (Eq.mpr (id mem_translate._simp_1) (Eq.mp mem_translate._simp_1 hq))hE0:¬measure E = 0⊢ ∑' (x : ↑ι), measure E = ∑' (q : ↑ι), measure (B q) A:Set ℝE:Set ℝhA:IsVitali AhE:MeasurableSet EhEA:E ⊆ Aι:Set ℚ := Ioc 0 1B:↑ι → Set ℝ := fun q => translate E ↑↑qhBdisj:Pairwise (Disjoint on B) := fun ⦃q r⦄ hqr => have this := disjoint_translate_of_subset hA hEA fun h => hqr (Subtype.ext h); disjoint_iff_inter_eq_empty.mpr thishBsub:⋃ q, B q ⊆ Icc 0 2 := fun ⦃x⦄ hx => Exists.casesOn (mem_iUnion.mp hx) fun q hq => translate_subset_Icc_zero_two (HasSubset.Subset.trans hEA hA.subset_Icc_zero_one) (↑↑q) (cast (Eq.trans (Eq.trans (congrFun' (congrArg LE.le (Eq.symm Nat.cast_zero)) ↑q) (congrFun' (congrArg LE.le Nat.cast_zero) ↑q)) (Eq.symm (Eq.trans (Eq.trans (congrFun' (congrArg LE.le (Eq.symm Nat.cast_zero)) ↑↑q) Rat.natCast_le_cast._simp_1) (congrFun' (congrArg LE.le Nat.cast_zero) ↑q)))) (le_of_lt q.property.left)) (cast (Eq.trans (Eq.trans (congrArg (LE.le ↑q) (Eq.symm Nat.cast_one)) (congrArg (LE.le ↑q) Nat.cast_one)) (Eq.symm (Eq.trans (Eq.trans (congrArg (LE.le ↑↑q) (Eq.symm Nat.cast_one)) Rat.cast_le_natCast._simp_1) (congrArg (LE.le ↑q) Nat.cast_one)))) q.property.right) (Eq.mpr (id mem_translate._simp_1) (Eq.mp mem_translate._simp_1 hq))hE0:¬measure E = 0q:↑ι⊢ measure E = measure (B q) All goals completed! 🐙 _ = measure (⋃ q, B q) := (measure_iUnion_countable hBdisj (fun q ↦ hE.translate _)).symm _ ≤ measure (Icc 0 2) := measure_mono hBsub _ = 2 := A:Set ℝE:Set ℝhA:IsVitali AhE:MeasurableSet EhEA:E ⊆ Aι:Set ℚ := Ioc 0 1B:↑ι → Set ℝ := fun q => translate E ↑↑qhBdisj:Pairwise (Disjoint on B) := fun ⦃q r⦄ hqr => have this := disjoint_translate_of_subset hA hEA fun h => hqr (Subtype.ext h); disjoint_iff_inter_eq_empty.mpr thishBsub:⋃ q, B q ⊆ Icc 0 2 := fun ⦃x⦄ hx => Exists.casesOn (mem_iUnion.mp hx) fun q hq => translate_subset_Icc_zero_two (HasSubset.Subset.trans hEA hA.subset_Icc_zero_one) (↑↑q) (cast (Eq.trans (Eq.trans (congrFun' (congrArg LE.le (Eq.symm Nat.cast_zero)) ↑q) (congrFun' (congrArg LE.le Nat.cast_zero) ↑q)) (Eq.symm (Eq.trans (Eq.trans (congrFun' (congrArg LE.le (Eq.symm Nat.cast_zero)) ↑↑q) Rat.natCast_le_cast._simp_1) (congrFun' (congrArg LE.le Nat.cast_zero) ↑q)))) (le_of_lt q.property.left)) (cast (Eq.trans (Eq.trans (congrArg (LE.le ↑q) (Eq.symm Nat.cast_one)) (congrArg (LE.le ↑q) Nat.cast_one)) (Eq.symm (Eq.trans (Eq.trans (congrArg (LE.le ↑↑q) (Eq.symm Nat.cast_one)) Rat.cast_le_natCast._simp_1) (congrArg (LE.le ↑q) Nat.cast_one)))) q.property.right) (Eq.mpr (id mem_translate._simp_1) (Eq.mp mem_translate._simp_1 hq))hE0:¬measure E = 0⊢ measure (Icc 0 2) = 2 All goals completed! 🐙

Taken together, the previous two lemmas show that a Vitali set cannot be measurable.

Theorem (Nonmeasurability of Vitali Sets).

If A is a Vitali set, then A is not measurable.

Lean code
theorem IsVitali.not_measurableSet {A : Set ℝ} (hA : IsVitali A) : ¬ MeasurableSet A := fun h ↦ hA.measure_ne_zero <| hA.measure_eq_zero_of_measurableSet_subset h subset_rfl
Lemma.

If A is a Vitali set, then m([0,1] \setminus A) = 1.

Lean code
theorem IsVitali.measure_compl_eq_one {A : Set ℝ} (hA : IsVitali A) : measure (Icc 0 1 \ A) = 1 := A:Set ℝhA:IsVitali A⊢ measure (Icc 0 1 \ A) = 1 A:Set ℝhA:IsVitali A⊢ measure (Icc 0 1 \ A) ≤ 1A:Set ℝhA:IsVitali A⊢ 1 ≤ measure (Icc 0 1 \ A) A:Set ℝhA:IsVitali A⊢ measure (Icc 0 1 \ A) ≤ 1 calc measure (Icc 0 1 \ A) ≤ measure (Icc 0 1) := measure_mono diff_subset _ = 1 := measure_Icc_zero_one A:Set ℝhA:IsVitali Ahlt:¬1 ≤ measure (Icc 0 1 \ A)⊢ False A:Set ℝhA:IsVitali Ahlt:¬1 ≤ measure (Icc 0 1 \ A)⊢ measure (Icc 0 1 \ A) = 1 A:Set ℝhA:IsVitali Ahlt:¬1 ≤ measure (Icc 0 1 \ A)E':Set ℝhE':Icc 0 1 \ A ⊆ E'hE'meas:MeasurableSet E'hE'eq:measure E' = measure (Icc 0 1 \ A)⊢ measure (Icc 0 1 \ A) = 1 A:Set ℝhA:IsVitali Ahlt:¬1 ≤ measure (Icc 0 1 \ A)E':Set ℝhE':Icc 0 1 \ A ⊆ E'hE'meas:MeasurableSet E'hE'eq:measure E' = measure (Icc 0 1 \ A)F:Set ℝ := E' ∩ Icc 0 1⊢ measure (Icc 0 1 \ A) = 1 A:Set ℝhA:IsVitali Ahlt:¬1 ≤ measure (Icc 0 1 \ A)E':Set ℝhE':Icc 0 1 \ A ⊆ E'hE'meas:MeasurableSet E'hE'eq:measure E' = measure (Icc 0 1 \ A)F:Set ℝ := E' ∩ Icc 0 1hBsubF:Icc 0 1 \ A ⊆ F := fun x hx => ⟨hE' hx, hx.left⟩⊢ measure (Icc 0 1 \ A) = 1 have hFeq : measure F = measure (Icc 0 1 \ A) := A:Set ℝhA:IsVitali A⊢ measure (Icc 0 1 \ A) = 1 A:Set ℝhA:IsVitali Ahlt:¬1 ≤ measure (Icc 0 1 \ A)E':Set ℝhE':Icc 0 1 \ A ⊆ E'hE'meas:MeasurableSet E'hE'eq:measure E' = measure (Icc 0 1 \ A)F:Set ℝ := E' ∩ Icc 0 1hBsubF:Icc 0 1 \ A ⊆ F := fun x hx => ⟨hE' hx, hx.left⟩⊢ measure F ≤ measure (Icc 0 1 \ A) calc measure F ≤ measure E' := measure_mono Set.inter_subset_left _ = measure (Icc 0 1 \ A) := hE'eq A:Set ℝhA:IsVitali Ahlt:¬1 ≤ measure (Icc 0 1 \ A)E':Set ℝhE':Icc 0 1 \ A ⊆ E'hE'meas:MeasurableSet E'hE'eq:measure E' = measure (Icc 0 1 \ A)F:Set ℝ := E' ∩ Icc 0 1hBsubF:Icc 0 1 \ A ⊆ F := fun x hx => ⟨hE' hx, hx.left⟩hFeq:measure F = measure (Icc 0 1 \ A) := le_antisymm (Trans.trans (measure_mono inter_subset_left) hE'eq) (measure_mono hBsubF)E:Set ℝ := Icc 0 1 \ F⊢ measure (Icc 0 1 \ A) = 1 A:Set ℝhA:IsVitali Ahlt:¬1 ≤ measure (Icc 0 1 \ A)E':Set ℝhE':Icc 0 1 \ A ⊆ E'hE'meas:MeasurableSet E'hE'eq:measure E' = measure (Icc 0 1 \ A)F:Set ℝ := E' ∩ Icc 0 1hBsubF:Icc 0 1 \ A ⊆ F := fun x hx => ⟨hE' hx, hx.left⟩hFeq:measure F = measure (Icc 0 1 \ A) := le_antisymm (Trans.trans (measure_mono inter_subset_left) hE'eq) (measure_mono hBsubF)E:Set ℝ := Icc 0 1 \ FhEmeas:MeasurableSet E := MeasurableSet.diff (measurableSet_Icc 0 1) (MeasurableSet.inter hE'meas (measurableSet_Icc 0 1))⊢ measure (Icc 0 1 \ A) = 1 have hEsubA : E ⊆ A := A:Set ℝhA:IsVitali A⊢ measure (Icc 0 1 \ A) = 1 intro x A:Set ℝhA:IsVitali Ahlt:¬1 ≤ measure (Icc 0 1 \ A)E':Set ℝhE':Icc 0 1 \ A ⊆ E'hE'meas:MeasurableSet E'hE'eq:measure E' = measure (Icc 0 1 \ A)F:Set ℝ := E' ∩ Icc 0 1hBsubF:Icc 0 1 \ A ⊆ F := fun x hx => ⟨hE' hx, hx.left⟩hFeq:measure F = measure (Icc 0 1 \ A) := le_antisymm (Trans.trans (measure_mono inter_subset_left) hE'eq) (measure_mono hBsubF)E:Set ℝ := Icc 0 1 \ FhEmeas:MeasurableSet E := MeasurableSet.diff (measurableSet_Icc 0 1) (MeasurableSet.inter hE'meas (measurableSet_Icc 0 1))x:ℝhx:x ∈ E⊢ x ∈ A A:Set ℝhA:IsVitali Ahlt:¬1 ≤ measure (Icc 0 1 \ A)E':Set ℝhE':Icc 0 1 \ A ⊆ E'hE'meas:MeasurableSet E'hE'eq:measure E' = measure (Icc 0 1 \ A)F:Set ℝ := E' ∩ Icc 0 1hBsubF:Icc 0 1 \ A ⊆ F := fun x hx => ⟨hE' hx, hx.left⟩hFeq:measure F = measure (Icc 0 1 \ A) := le_antisymm (Trans.trans (measure_mono inter_subset_left) hE'eq) (measure_mono hBsubF)E:Set ℝ := Icc 0 1 \ FhEmeas:MeasurableSet E := MeasurableSet.diff (measurableSet_Icc 0 1) (MeasurableSet.inter hE'meas (measurableSet_Icc 0 1))x:ℝhx:x ∈ EhxA:x ∉ A⊢ False A:Set ℝhA:IsVitali Ahlt:¬1 ≤ measure (Icc 0 1 \ A)E':Set ℝhE':Icc 0 1 \ A ⊆ E'hE'meas:MeasurableSet E'hE'eq:measure E' = measure (Icc 0 1 \ A)F:Set ℝ := E' ∩ Icc 0 1hBsubF:Icc 0 1 \ A ⊆ F := fun x hx => ⟨hE' hx, hx.left⟩hFeq:measure F = measure (Icc 0 1 \ A) := le_antisymm (Trans.trans (measure_mono inter_subset_left) hE'eq) (measure_mono hBsubF)E:Set ℝ := Icc 0 1 \ FhEmeas:MeasurableSet E := MeasurableSet.diff (measurableSet_Icc 0 1) (MeasurableSet.inter hE'meas (measurableSet_Icc 0 1))x:ℝhx:x ∈ EhxA:x ∉ Ahxdiff:x ∈ Icc 0 1 \ A := ⟨hx.left, hxA⟩⊢ False A:Set ℝhA:IsVitali Ahlt:¬1 ≤ measure (Icc 0 1 \ A)E':Set ℝhE':Icc 0 1 \ A ⊆ E'hE'meas:MeasurableSet E'hE'eq:measure E' = measure (Icc 0 1 \ A)F:Set ℝ := E' ∩ Icc 0 1hBsubF:Icc 0 1 \ A ⊆ F := fun x hx => ⟨hE' hx, hx.left⟩hFeq:measure F = measure (Icc 0 1 \ A) := le_antisymm (Trans.trans (measure_mono inter_subset_left) hE'eq) (measure_mono hBsubF)E:Set ℝ := Icc 0 1 \ FhEmeas:MeasurableSet E := MeasurableSet.diff (measurableSet_Icc 0 1) (MeasurableSet.inter hE'meas (measurableSet_Icc 0 1))x:ℝhx:x ∈ EhxA:x ∉ Ahxdiff:x ∈ Icc 0 1 \ A := ⟨hx.left, hxA⟩hxF:x ∈ F := ⟨hE' hxdiff, hx.left⟩⊢ False All goals completed! 🐙 have hEF : E ∩ F = ∅ := Set.disjoint_iff_inter_eq_empty.1 (A:Set ℝhA:IsVitali Ahlt:¬1 ≤ measure (Icc 0 1 \ A)E':Set ℝhE':Icc 0 1 \ A ⊆ E'hE'meas:MeasurableSet E'hE'eq:measure E' = measure (Icc 0 1 \ A)F:Set ℝ := E' ∩ Icc 0 1hBsubF:Icc 0 1 \ A ⊆ F := fun x hx => ⟨hE' hx, hx.left⟩hFeq:measure F = measure (Icc 0 1 \ A) := le_antisymm (Trans.trans (measure_mono inter_subset_left) hE'eq) (measure_mono hBsubF)E:Set ℝ := Icc 0 1 \ FhEmeas:MeasurableSet E := MeasurableSet.diff (measurableSet_Icc 0 1) (MeasurableSet.inter hE'meas (measurableSet_Icc 0 1))hEsubA:E ⊆ A := fun ⦃x⦄ hx => Classical.byContradiction fun hxA => have hxdiff := ⟨hx.left, hxA⟩; have hxF := ⟨hE' hxdiff, hx.left⟩; hx.right hxF⊢ Disjoint E F All goals completed! 🐙) calc measure (Icc 0 1 \ A) = measure F := hFeq.symm _ = measure E + measure F := A:Set ℝhA:IsVitali Ahlt:¬1 ≤ measure (Icc 0 1 \ A)E':Set ℝhE':Icc 0 1 \ A ⊆ E'hE'meas:MeasurableSet E'hE'eq:measure E' = measure (Icc 0 1 \ A)F:Set ℝ := E' ∩ Icc 0 1hBsubF:Icc 0 1 \ A ⊆ F := fun x hx => ⟨hE' hx, hx.left⟩hFeq:measure F = measure (Icc 0 1 \ A) := le_antisymm (Trans.trans (measure_mono inter_subset_left) hE'eq) (measure_mono hBsubF)E:Set ℝ := Icc 0 1 \ FhEmeas:MeasurableSet E := MeasurableSet.diff (measurableSet_Icc 0 1) (MeasurableSet.inter hE'meas (measurableSet_Icc 0 1))hEsubA:E ⊆ A := fun ⦃x⦄ hx => Classical.byContradiction fun hxA => have hxdiff := ⟨hx.left, hxA⟩; have hxF := ⟨hE' hxdiff, hx.left⟩; hx.right hxFhEF:E ∩ F = ∅ := disjoint_iff_inter_eq_empty.mp (measure_compl_eq_one._proof_1 E')⊢ measure F = measure E + measure F All goals completed! 🐙 _ = measure (E ∪ F) := A:Set ℝhA:IsVitali Ahlt:¬1 ≤ measure (Icc 0 1 \ A)E':Set ℝhE':Icc 0 1 \ A ⊆ E'hE'meas:MeasurableSet E'hE'eq:measure E' = measure (Icc 0 1 \ A)F:Set ℝ := E' ∩ Icc 0 1hBsubF:Icc 0 1 \ A ⊆ F := fun x hx => ⟨hE' hx, hx.left⟩hFeq:measure F = measure (Icc 0 1 \ A) := le_antisymm (Trans.trans (measure_mono inter_subset_left) hE'eq) (measure_mono hBsubF)E:Set ℝ := Icc 0 1 \ FhEmeas:MeasurableSet E := MeasurableSet.diff (measurableSet_Icc 0 1) (MeasurableSet.inter hE'meas (measurableSet_Icc 0 1))hEsubA:E ⊆ A := fun ⦃x⦄ hx => Classical.byContradiction fun hxA => have hxdiff := ⟨hx.left, hxA⟩; have hxF := ⟨hE' hxdiff, hx.left⟩; hx.right hxFhEF:E ∩ F = ∅ := disjoint_iff_inter_eq_empty.mp (measure_compl_eq_one._proof_1 E')⊢ measure E + measure F = measure (E ∪ F) All goals completed! 🐙 _ = measure (Icc 0 1) := A:Set ℝhA:IsVitali Ahlt:¬1 ≤ measure (Icc 0 1 \ A)E':Set ℝhE':Icc 0 1 \ A ⊆ E'hE'meas:MeasurableSet E'hE'eq:measure E' = measure (Icc 0 1 \ A)F:Set ℝ := E' ∩ Icc 0 1hBsubF:Icc 0 1 \ A ⊆ F := fun x hx => ⟨hE' hx, hx.left⟩hFeq:measure F = measure (Icc 0 1 \ A) := le_antisymm (Trans.trans (measure_mono inter_subset_left) hE'eq) (measure_mono hBsubF)E:Set ℝ := Icc 0 1 \ FhEmeas:MeasurableSet E := MeasurableSet.diff (measurableSet_Icc 0 1) (MeasurableSet.inter hE'meas (measurableSet_Icc 0 1))hEsubA:E ⊆ A := fun ⦃x⦄ hx => Classical.byContradiction fun hxA => have hxdiff := ⟨hx.left, hxA⟩; have hxF := ⟨hE' hxdiff, hx.left⟩; hx.right hxFhEF:E ∩ F = ∅ := disjoint_iff_inter_eq_empty.mp (measure_compl_eq_one._proof_1 E')⊢ measure (E ∪ F) = measure (Icc 0 1) All goals completed! 🐙 _ = 1 := measure_Icc_zero_one
Theorem (Failure of Additivity for Vitali Sets).

If A is a Vitali set, then m([0,1]) \neq m(A) + m([0,1] \setminus A).

Lean code
theorem IsVitali.compl_nonadditive {A : Set ℝ} (hA : IsVitali A) : measure (Icc 0 1) ≠ measure A + measure (Icc 0 1 \ A) := A:Set ℝhA:IsVitali A⊢ measure (Icc 0 1) ≠ measure A + measure (Icc 0 1 \ A) A:Set ℝhA:IsVitali A⊢ measure (Icc 0 1) < measure A + measure (Icc 0 1 \ A) calc measure (Icc 0 1) = 1 := measure_Icc_zero_one _ < measure A + 1 := A:Set ℝhA:IsVitali A⊢ 1 < measure A + 1 simpa [add_comm] using ENNReal.lt_add_right (A:Set ℝhA:IsVitali A⊢ 1 ≠ ∞ All goals completed! 🐙) hA.measure_ne_zero _ = measure A + measure (Icc 0 1 \ A) := A:Set ℝhA:IsVitali A⊢ measure A + 1 = measure A + measure (Icc 0 1 \ A) All goals completed! 🐙

To deduce actual existence statements, it remains only to construct one Vitali set.

Definition (Existence of Vitali Sets).

Consider the equivalence relation on \mathbb{R} given by rational translation. Every equivalence class meets [0,1], so by the axiom of choice we may choose one point in [0,1] from each class. Let V \subseteq \mathbb{R} be the set of all chosen representatives.

Lean code
theorem exists_rationalRel_mem_Icc_zero_one (x : ℝ) : ∃ y : (Icc 0 1 : Set ℝ), rationalRel x y := x:ℝ⊢ ∃ y, rationalRel x ↑y x:ℝq:ℚhq_left:x - 1 < ↑qhq_right:↑q < x⊢ ∃ y, rationalRel x ↑y refine ⟨⟨x - q, x:ℝq:ℚhq_left:x - 1 < ↑qhq_right:↑q < x⊢ x - ↑q ∈ Icc 0 1 All goals completed! 🐙⟩, ⟨q, x:ℝq:ℚhq_left:x - 1 < ↑qhq_right:↑q < x⊢ x - ↑⟨x - ↑q, ⋯⟩ = ↑q All goals completed! 🐙⟩⟩
theorem exists_subtype_mk_eq_quotient (q : Quotient rationalRelSetoid) : ∃ y : (Icc 0 1 : Set ℝ), ⟦(y : ℝ)⟧ = q := q:Quotient rationalRelSetoid⊢ ∃ y, ⟦↑y⟧ = q q:Quotient rationalRelSetoid⊢ ∀ (a : ℝ), ∃ y, ⟦↑y⟧ = ⟦a⟧ q:Quotient rationalRelSetoidx:ℝ⊢ ∃ y, ⟦↑y⟧ = ⟦x⟧ q:Quotient rationalRelSetoidx:ℝy:↑(Icc 0 1)hy:rationalRel x ↑y⊢ ∃ y, ⟦↑y⟧ = ⟦x⟧ All goals completed! 🐙
def chosenVitaliPoint (q : Quotient rationalRelSetoid) : (Icc 0 1 : Set ℝ) := Classical.choose (exists_subtype_mk_eq_quotient q)
def chosenVitali : Set ℝ := Set.range fun q : Quotient rationalRelSetoid ↦ (chosenVitaliPoint q : ℝ)
Lemma.

The set V defined above is a Vitali set.

Lean code
theorem chosenVitali_subset_Icc_zero_one : chosenVitali ⊆ Icc 0 1 := ⊢ chosenVitali ⊆ Icc 0 1 q:Quotient rationalRelSetoid⊢ (fun q => ↑(chosenVitaliPoint q)) q ∈ Icc 0 1 All goals completed! 🐙
theorem existsUnique_rational_chosenVitali (x : ℝ) : ∃! q : ℚ, x - q ∈ chosenVitali := x:ℝ⊢ ∃! q, x - ↑q ∈ chosenVitali x:ℝq:ℚhq:x - ↑(chosenVitaliPoint ⟦x⟧) = ↑q⊢ ∃! q, x - ↑q ∈ chosenVitali refine ⟨q, ⟨⟦x⟧, x:ℝq:ℚhq:x - ↑(chosenVitaliPoint ⟦x⟧) = ↑q⊢ (fun q => ↑(chosenVitaliPoint q)) ⟦x⟧ = x - ↑q All goals completed! 🐙⟩, ?_⟩ intro r x:ℝq:ℚhq:x - ↑(chosenVitaliPoint ⟦x⟧) = ↑qr:ℚhr:x - ↑r ∈ chosenVitali⊢ r = q have hz : x - r = chosenVitaliPoint ⟦x⟧ := eq_chosenVitaliPoint_of_mem_chosenVitali_of_rationalRel hr ⟨r, x:ℝq:ℚhq:x - ↑(chosenVitaliPoint ⟦x⟧) = ↑qr:ℚhr:x - ↑r ∈ chosenVitali⊢ x - (x - ↑r) = ↑r All goals completed! 🐙⟩ exact Rat.cast_inj.mp <| calc (r : ℝ) = x - (chosenVitaliPoint ⟦x⟧ : ℝ) := x:ℝq:ℚhq:x - ↑(chosenVitaliPoint ⟦x⟧) = ↑qr:ℚhr:x - ↑r ∈ chosenVitalihz:x - ↑r = ↑(chosenVitaliPoint ⟦x⟧) := eq_chosenVitaliPoint_of_mem_chosenVitali_of_rationalRel hr (Exists.intro r (Mathlib.Tactic.Ring.of_eq (Mathlib.Tactic.Ring.sub_congr (Mathlib.Tactic.Ring.atom_pf x) (Mathlib.Tactic.Ring.sub_congr (Mathlib.Tactic.Ring.atom_pf x) (Mathlib.Tactic.Ring.atom_pf ↑r) (Mathlib.Tactic.Ring.sub_pf (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_mul (↑r) (Nat.rawCast 1) (Mathlib.Tactic.Ring.neg_one_mul (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 1)) (Eq.refl (Int.negOfNat 1)))))) Mathlib.Tactic.Ring.neg_zero) (Mathlib.Tactic.Ring.add_pf_add_lt (x ^ Nat.rawCast 1 * Nat.rawCast 1) (Mathlib.Tactic.Ring.add_pf_zero_add (↑r ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast + 0))))) (Mathlib.Tactic.Ring.sub_pf (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_mul x (Nat.rawCast 1) (Mathlib.Tactic.Ring.neg_one_mul (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 1)) (Eq.refl (Int.negOfNat 1)))))) (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_mul (↑r) (Nat.rawCast 1) (Mathlib.Tactic.Ring.neg_one_mul (Mathlib.Meta.NormNum.IsNat.to_raw_eq (Mathlib.Meta.NormNum.IsInt.to_isNat (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 1)) (Eq.refl (Int.ofNat 1))))))) Mathlib.Tactic.Ring.neg_zero)) (Mathlib.Tactic.Ring.add_pf_add_overlap_zero (Mathlib.Tactic.Ring.add_overlap_pf_zero x (Nat.rawCast 1) (Mathlib.Meta.NormNum.IsInt.to_isNat (Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 1)) (Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 1)) (Eq.refl (Int.ofNat 0))))) (Mathlib.Tactic.Ring.add_pf_zero_add (↑r ^ Nat.rawCast 1 * Nat.rawCast 1 + 0))))) (Mathlib.Tactic.Ring.atom_pf ↑r)))⊢ ↑r = x - ↑(chosenVitaliPoint ⟦x⟧) All goals completed! 🐙 _ = (q : ℝ) := x:ℝq:ℚhq:x - ↑(chosenVitaliPoint ⟦x⟧) = ↑qr:ℚhr:x - ↑r ∈ chosenVitalihz:x - ↑r = ↑(chosenVitaliPoint ⟦x⟧) := eq_chosenVitaliPoint_of_mem_chosenVitali_of_rationalRel hr (Exists.intro r (Mathlib.Tactic.Ring.of_eq (Mathlib.Tactic.Ring.sub_congr (Mathlib.Tactic.Ring.atom_pf x) (Mathlib.Tactic.Ring.sub_congr (Mathlib.Tactic.Ring.atom_pf x) (Mathlib.Tactic.Ring.atom_pf ↑r) (Mathlib.Tactic.Ring.sub_pf (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_mul (↑r) (Nat.rawCast 1) (Mathlib.Tactic.Ring.neg_one_mul (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 1)) (Eq.refl (Int.negOfNat 1)))))) Mathlib.Tactic.Ring.neg_zero) (Mathlib.Tactic.Ring.add_pf_add_lt (x ^ Nat.rawCast 1 * Nat.rawCast 1) (Mathlib.Tactic.Ring.add_pf_zero_add (↑r ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast + 0))))) (Mathlib.Tactic.Ring.sub_pf (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_mul x (Nat.rawCast 1) (Mathlib.Tactic.Ring.neg_one_mul (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 1)) (Eq.refl (Int.negOfNat 1)))))) (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_mul (↑r) (Nat.rawCast 1) (Mathlib.Tactic.Ring.neg_one_mul (Mathlib.Meta.NormNum.IsNat.to_raw_eq (Mathlib.Meta.NormNum.IsInt.to_isNat (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 1)) (Eq.refl (Int.ofNat 1))))))) Mathlib.Tactic.Ring.neg_zero)) (Mathlib.Tactic.Ring.add_pf_add_overlap_zero (Mathlib.Tactic.Ring.add_overlap_pf_zero x (Nat.rawCast 1) (Mathlib.Meta.NormNum.IsInt.to_isNat (Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 1)) (Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 1)) (Eq.refl (Int.ofNat 0))))) (Mathlib.Tactic.Ring.add_pf_zero_add (↑r ^ Nat.rawCast 1 * Nat.rawCast 1 + 0))))) (Mathlib.Tactic.Ring.atom_pf ↑r)))⊢ x - ↑(chosenVitaliPoint ⟦x⟧) = ↑q All goals completed! 🐙
theorem isVitali_chosenVitali : IsVitali chosenVitali := ⟨existsUnique_rational_chosenVitali, chosenVitali_subset_Icc_zero_one⟩
Theorem (Existence of Nonmeasurable Sets).

There exists a set A \subseteq \mathbb{R} that is not measurable.

Lean code
theorem exists_not_measurableSet : ∃ A : Set ℝ, ¬ MeasurableSet A := ⟨chosenVitali, isVitali_chosenVitali.not_measurableSet⟩
Theorem (Failure of Additivity).

There exist disjoint sets A, B \subseteq \mathbb{R} such that m(A \cup B) \neq m(A) + m(B).

Lean code
theorem exists_disjoint_nonadditive : ∃ A B : Set ℝ, A ∩ B = ∅ ∧ measure (A ∪ B) ≠ measure A + measure B := ⊢ ∃ A B, A ∩ B = ∅ ∧ measure (A ∪ B) ≠ measure A + measure B refine ⟨chosenVitali, Icc 0 1 \ chosenVitali, ⊢ chosenVitali ∩ (Icc 0 1 \ chosenVitali) = ∅ All goals completed! 🐙, ?_⟩ All goals completed! 🐙