測度論と積分

2.4. 可測集合はカラテオドリ🔗

補題.

任意の c \in \mathbb{R} に対して、半直線 [c,\infty) はカラテオドリである。

Lean code
theorem isCaratheodory_Ici (c : ℝ) : IsCaratheodory (Ici c) := c:ℝ⊢ IsCaratheodory (Ici c) c:ℝ⊢ ∀ (B : Set ℝ), measure (B ∩ Ici c) + measure (B \ Ici c) ≤ measure B c:ℝA:Set ℝ⊢ measure (A ∩ Ici c) + measure (A \ Ici c) ≤ measure A c:ℝA:Set ℝa:ℕ → ℝb:ℕ → ℝh:A ⊆ ⋃ i, Ioo (a i) (b i)⊢ measure (A ∩ Ici c) + measure (A \ Ici c) ≤ ∑' (i : ℕ), ENNReal.ofReal (b i - a i) calc measure (A ∩ Ici c) + measure (A \ Ici c) _ ≤ measure (⋃ i, Ioo (a i) (b i) ∩ Ici c) + measure (⋃ i, Ioo (a i) (b i) \ Ici c) := c:ℝA:Set ℝa:ℕ → ℝb:ℕ → ℝh:A ⊆ ⋃ i, Ioo (a i) (b i)⊢ measure (A ∩ Ici c) + measure (A \ Ici c) ≤ measure (⋃ i, Ioo (a i) (b i) ∩ Ici c) + measure (⋃ i, Ioo (a i) (b i) \ Ici c) c:ℝA:Set ℝa:ℕ → ℝb:ℕ → ℝh:A ⊆ ⋃ i, Ioo (a i) (b i)⊢ measure (A ∩ Ici c) ≤ measure (⋃ i, Ioo (a i) (b i) ∩ Ici c)c:ℝA:Set ℝa:ℕ → ℝb:ℕ → ℝh:A ⊆ ⋃ i, Ioo (a i) (b i)⊢ measure (A \ Ici c) ≤ measure (⋃ i, Ioo (a i) (b i) \ Ici c) c:ℝA:Set ℝa:ℕ → ℝb:ℕ → ℝh:A ⊆ ⋃ i, Ioo (a i) (b i)⊢ measure (A ∩ Ici c) ≤ measure (⋃ i, Ioo (a i) (b i) ∩ Ici c) c:ℝA:Set ℝa:ℕ → ℝb:ℕ → ℝh:A ⊆ ⋃ i, Ioo (a i) (b i)⊢ A ∩ Ici c ⊆ ⋃ i, Ioo (a i) (b i) ∩ Ici c c:ℝA:Set ℝa:ℕ → ℝb:ℕ → ℝh:A ⊆ ⋃ i, Ioo (a i) (b i)⊢ A ∩ Ici c ⊆ (⋃ i, Ioo (a i) (b i)) ∩ Ici c c:ℝA:Set ℝa:ℕ → ℝb:ℕ → ℝh:A ⊆ ⋃ i, Ioo (a i) (b i)⊢ A ⊆ ⋃ i, Ioo (a i) (b i) All goals completed! 🐙 c:ℝA:Set ℝa:ℕ → ℝb:ℕ → ℝh:A ⊆ ⋃ i, Ioo (a i) (b i)⊢ measure (A \ Ici c) ≤ measure (⋃ i, Ioo (a i) (b i) \ Ici c) c:ℝA:Set ℝa:ℕ → ℝb:ℕ → ℝh:A ⊆ ⋃ i, Ioo (a i) (b i)⊢ A \ Ici c ⊆ ⋃ i, Ioo (a i) (b i) \ Ici c c:ℝA:Set ℝa:ℕ → ℝb:ℕ → ℝh:A ⊆ ⋃ i, Ioo (a i) (b i)⊢ A \ Ici c ⊆ (⋃ i, Ioo (a i) (b i)) \ Ici c c:ℝA:Set ℝa:ℕ → ℝb:ℕ → ℝh:A ⊆ ⋃ i, Ioo (a i) (b i)⊢ A ⊆ ⋃ i, Ioo (a i) (b i) All goals completed! 🐙 _ ≤ ∑' (i : ℕ), measure (Ioo (a i) (b i) ∩ Ici c) + ∑' (i : ℕ), measure (Ioo (a i) (b i) \ Ici c) := c:ℝA:Set ℝa:ℕ → ℝb:ℕ → ℝh:A ⊆ ⋃ i, Ioo (a i) (b i)⊢ measure (⋃ i, Ioo (a i) (b i) ∩ Ici c) + measure (⋃ i, Ioo (a i) (b i) \ Ici c) ≤ ∑' (i : ℕ), measure (Ioo (a i) (b i) ∩ Ici c) + ∑' (i : ℕ), measure (Ioo (a i) (b i) \ Ici c) c:ℝA:Set ℝa:ℕ → ℝb:ℕ → ℝh:A ⊆ ⋃ i, Ioo (a i) (b i)⊢ measure (⋃ i, Ioo (a i) (b i) ∩ Ici c) ≤ ∑' (i : ℕ), measure (Ioo (a i) (b i) ∩ Ici c)c:ℝA:Set ℝa:ℕ → ℝb:ℕ → ℝh:A ⊆ ⋃ i, Ioo (a i) (b i)⊢ measure (⋃ i, Ioo (a i) (b i) \ Ici c) ≤ ∑' (i : ℕ), measure (Ioo (a i) (b i) \ Ici c) c:ℝA:Set ℝa:ℕ → ℝb:ℕ → ℝh:A ⊆ ⋃ i, Ioo (a i) (b i)⊢ measure (⋃ i, Ioo (a i) (b i) ∩ Ici c) ≤ ∑' (i : ℕ), measure (Ioo (a i) (b i) ∩ Ici c) All goals completed! 🐙 c:ℝA:Set ℝa:ℕ → ℝb:ℕ → ℝh:A ⊆ ⋃ i, Ioo (a i) (b i)⊢ measure (⋃ i, Ioo (a i) (b i) \ Ici c) ≤ ∑' (i : ℕ), measure (Ioo (a i) (b i) \ Ici c) All goals completed! 🐙 _ = ∑' (i : ℕ), (measure (Ioo (a i) (b i) ∩ Ici c) + measure (Ioo (a i) (b i) \ Ici c)) := c:ℝA:Set ℝa:ℕ → ℝb:ℕ → ℝh:A ⊆ ⋃ i, Ioo (a i) (b i)⊢ ∑' (i : ℕ), measure (Ioo (a i) (b i) ∩ Ici c) + ∑' (i : ℕ), measure (Ioo (a i) (b i) \ Ici c) = ∑' (i : ℕ), (measure (Ioo (a i) (b i) ∩ Ici c) + measure (Ioo (a i) (b i) \ Ici c)) All goals completed! 🐙 _ ≤ ∑' (i : ℕ), .ofReal (b i - a i) := c:ℝA:Set ℝa:ℕ → ℝb:ℕ → ℝh:A ⊆ ⋃ i, Ioo (a i) (b i)⊢ ∑' (i : ℕ), (measure (Ioo (a i) (b i) ∩ Ici c) + measure (Ioo (a i) (b i) \ Ici c)) ≤ ∑' (i : ℕ), ENNReal.ofReal (b i - a i) c:ℝA:Set ℝa:ℕ → ℝb:ℕ → ℝh:A ⊆ ⋃ i, Ioo (a i) (b i)⊢ ∀ (a_1 : ℕ), measure (Ioo (a a_1) (b a_1) ∩ Ici c) + measure (Ioo (a a_1) (b a_1) \ Ici c) ≤ ENNReal.ofReal (b a_1 - a a_1) c:ℝA:Set ℝa:ℕ → ℝb:ℕ → ℝh:A ⊆ ⋃ i, Ioo (a i) (b i)i:ℕ⊢ measure (Ioo (a i) (b i) ∩ Ici c) + measure (Ioo (a i) (b i) \ Ici c) ≤ ENNReal.ofReal (b i - a i) c:ℝA:Set ℝa:ℕ → ℝb:ℕ → ℝh:A ⊆ ⋃ i, Ioo (a i) (b i)i:ℕhac:a i < c⊢ measure (Ioo (a i) (b i) ∩ Ici c) + measure (Ioo (a i) (b i) \ Ici c) ≤ ENNReal.ofReal (b i - a i)c:ℝA:Set ℝa:ℕ → ℝb:ℕ → ℝh:A ⊆ ⋃ i, Ioo (a i) (b i)i:ℕhac:c ≤ a i⊢ measure (Ioo (a i) (b i) ∩ Ici c) + measure (Ioo (a i) (b i) \ Ici c) ≤ ENNReal.ofReal (b i - a i) c:ℝA:Set ℝa:ℕ → ℝb:ℕ → ℝh:A ⊆ ⋃ i, Ioo (a i) (b i)i:ℕhac:a i < c⊢ measure (Ioo (a i) (b i) ∩ Ici c) + measure (Ioo (a i) (b i) \ Ici c) ≤ ENNReal.ofReal (b i - a i)c:ℝA:Set ℝa:ℕ → ℝb:ℕ → ℝh:A ⊆ ⋃ i, Ioo (a i) (b i)i:ℕhac:c ≤ a i⊢ measure (Ioo (a i) (b i) ∩ Ici c) + measure (Ioo (a i) (b i) \ Ici c) ≤ ENNReal.ofReal (b i - a i) c:ℝA:Set ℝa:ℕ → ℝb:ℕ → ℝh:A ⊆ ⋃ i, Ioo (a i) (b i)i:ℕhac:c ≤ a ihbc:b i < c⊢ measure (Ioo (a i) (b i) ∩ Ici c) + measure (Ioo (a i) (b i) \ Ici c) ≤ ENNReal.ofReal (b i - a i)c:ℝA:Set ℝa:ℕ → ℝb:ℕ → ℝh:A ⊆ ⋃ i, Ioo (a i) (b i)i:ℕhac:c ≤ a ihbc:c ≤ b i⊢ measure (Ioo (a i) (b i) ∩ Ici c) + measure (Ioo (a i) (b i) \ Ici c) ≤ ENNReal.ofReal (b i - a i) c:ℝA:Set ℝa:ℕ → ℝb:ℕ → ℝh:A ⊆ ⋃ i, Ioo (a i) (b i)i:ℕhac:a i < chbc:b i < c⊢ measure (Ioo (a i) (b i) ∩ Ici c) + measure (Ioo (a i) (b i) \ Ici c) ≤ ENNReal.ofReal (b i - a i) have : Ioo (a i) (b i) ∩ Ici c = ∅ := c:ℝA:Set ℝa:ℕ → ℝb:ℕ → ℝh:A ⊆ ⋃ i, Ioo (a i) (b i)⊢ ∑' (i : ℕ), (measure (Ioo (a i) (b i) ∩ Ici c) + measure (Ioo (a i) (b i) \ Ici c)) ≤ ∑' (i : ℕ), ENNReal.ofReal (b i - a i) All goals completed! 🐙 c:ℝA:Set ℝa:ℕ → ℝb:ℕ → ℝh:A ⊆ ⋃ i, Ioo (a i) (b i)i:ℕhac:a i < chbc:b i < cthis:Ioo (a i) (b i) ∩ Ici c = ∅ := isCaratheodory_Ici._proof_1 c a b i hbc⊢ measure ∅ + measure (Ioo (a i) (b i) \ Ici c) ≤ ENNReal.ofReal (b i - a i) have : Ioo (a i) (b i) \ Ici c = Ioo (a i) (b i) := c:ℝA:Set ℝa:ℕ → ℝb:ℕ → ℝh:A ⊆ ⋃ i, Ioo (a i) (b i)⊢ ∑' (i : ℕ), (measure (Ioo (a i) (b i) ∩ Ici c) + measure (Ioo (a i) (b i) \ Ici c)) ≤ ∑' (i : ℕ), ENNReal.ofReal (b i - a i) All goals completed! 🐙 c:ℝA:Set ℝa:ℕ → ℝb:ℕ → ℝh:A ⊆ ⋃ i, Ioo (a i) (b i)i:ℕhac:a i < chbc:b i < cthis✝:Ioo (a i) (b i) ∩ Ici c = ∅ := isCaratheodory_Ici._proof_1 c a b i hbcthis:Ioo (a i) (b i) \ Ici c = Ioo (a i) (b i) := isCaratheodory_Ici._proof_2 c a b i hbc⊢ measure ∅ + measure (Ioo (a i) (b i)) ≤ ENNReal.ofReal (b i - a i) c:ℝA:Set ℝa:ℕ → ℝb:ℕ → ℝh:A ⊆ ⋃ i, Ioo (a i) (b i)i:ℕhac:a i < chbc:b i < cthis✝:Ioo (a i) (b i) ∩ Ici c = ∅ := isCaratheodory_Ici._proof_1 c a b i hbcthis:Ioo (a i) (b i) \ Ici c = Ioo (a i) (b i) := isCaratheodory_Ici._proof_2 c a b i hbc⊢ measure (Ioo (a i) (b i)) ≤ ENNReal.ofReal (b i - a i) All goals completed! 🐙 c:ℝA:Set ℝa:ℕ → ℝb:ℕ → ℝh:A ⊆ ⋃ i, Ioo (a i) (b i)i:ℕhac:a i < chbc:c ≤ b i⊢ measure (Ioo (a i) (b i) ∩ Ici c) + measure (Ioo (a i) (b i) \ Ici c) ≤ ENNReal.ofReal (b i - a i) have : Ioo (a i) (b i) ∩ Ici c = Ico c (b i) := c:ℝA:Set ℝa:ℕ → ℝb:ℕ → ℝh:A ⊆ ⋃ i, Ioo (a i) (b i)⊢ ∑' (i : ℕ), (measure (Ioo (a i) (b i) ∩ Ici c) + measure (Ioo (a i) (b i) \ Ici c)) ≤ ∑' (i : ℕ), ENNReal.ofReal (b i - a i) All goals completed! 🐙 c:ℝA:Set ℝa:ℕ → ℝb:ℕ → ℝh:A ⊆ ⋃ i, Ioo (a i) (b i)i:ℕhac:a i < chbc:c ≤ b ithis:Ioo (a i) (b i) ∩ Ici c = Ico c (b i) := isCaratheodory_Ici._proof_3 c a b i hac⊢ measure (Ico c (b i)) + measure (Ioo (a i) (b i) \ Ici c) ≤ ENNReal.ofReal (b i - a i) have : Ioo (a i) (b i) \ Ici c = Ioo (a i) c := c:ℝA:Set ℝa:ℕ → ℝb:ℕ → ℝh:A ⊆ ⋃ i, Ioo (a i) (b i)⊢ ∑' (i : ℕ), (measure (Ioo (a i) (b i) ∩ Ici c) + measure (Ioo (a i) (b i) \ Ici c)) ≤ ∑' (i : ℕ), ENNReal.ofReal (b i - a i) All goals completed! 🐙 c:ℝA:Set ℝa:ℕ → ℝb:ℕ → ℝh:A ⊆ ⋃ i, Ioo (a i) (b i)i:ℕhac:a i < chbc:c ≤ b ithis✝:Ioo (a i) (b i) ∩ Ici c = Ico c (b i) := isCaratheodory_Ici._proof_3 c a b i hacthis:Ioo (a i) (b i) \ Ici c = Ioo (a i) c := isCaratheodory_Ici._proof_4 c a b i hbc⊢ measure (Ico c (b i)) + measure (Ioo (a i) c) ≤ ENNReal.ofReal (b i - a i) c:ℝA:Set ℝa:ℕ → ℝb:ℕ → ℝh:A ⊆ ⋃ i, Ioo (a i) (b i)i:ℕhac:a i < chbc:c ≤ b ithis✝:Ioo (a i) (b i) ∩ Ici c = Ico c (b i) := isCaratheodory_Ici._proof_3 c a b i hacthis:Ioo (a i) (b i) \ Ici c = Ioo (a i) c := isCaratheodory_Ici._proof_4 c a b i hbc⊢ ENNReal.ofReal (b i - c) + ENNReal.ofReal (c - a i) ≤ ENNReal.ofReal (b i - a i) c:ℝA:Set ℝa:ℕ → ℝb:ℕ → ℝh:A ⊆ ⋃ i, Ioo (a i) (b i)i:ℕhac:a i < chbc:c ≤ b ithis✝:Ioo (a i) (b i) ∩ Ici c = Ico c (b i) := isCaratheodory_Ici._proof_3 c a b i hacthis:Ioo (a i) (b i) \ Ici c = Ioo (a i) c := isCaratheodory_Ici._proof_4 c a b i hbc⊢ ENNReal.ofReal (b i - c) + ENNReal.ofReal (c - a i) = ENNReal.ofReal (b i - a i) c:ℝA:Set ℝa:ℕ → ℝb:ℕ → ℝh:A ⊆ ⋃ i, Ioo (a i) (b i)i:ℕhac:a i < chbc:c ≤ b ithis✝:Ioo (a i) (b i) ∩ Ici c = Ico c (b i) := isCaratheodory_Ici._proof_3 c a b i hacthis:Ioo (a i) (b i) \ Ici c = Ioo (a i) c := isCaratheodory_Ici._proof_4 c a b i hbc⊢ ENNReal.ofReal (b i - c + (c - a i)) = ENNReal.ofReal (b i - a i) All goals completed! 🐙 c:ℝA:Set ℝa:ℕ → ℝb:ℕ → ℝh:A ⊆ ⋃ i, Ioo (a i) (b i)i:ℕhac:c ≤ a ihbc:b i < c⊢ measure (Ioo (a i) (b i) ∩ Ici c) + measure (Ioo (a i) (b i) \ Ici c) ≤ ENNReal.ofReal (b i - a i) have : Ioo (a i) (b i) = ∅ := c:ℝA:Set ℝa:ℕ → ℝb:ℕ → ℝh:A ⊆ ⋃ i, Ioo (a i) (b i)⊢ ∑' (i : ℕ), (measure (Ioo (a i) (b i) ∩ Ici c) + measure (Ioo (a i) (b i) \ Ici c)) ≤ ∑' (i : ℕ), ENNReal.ofReal (b i - a i) All goals completed! 🐙 All goals completed! 🐙 c:ℝA:Set ℝa:ℕ → ℝb:ℕ → ℝh:A ⊆ ⋃ i, Ioo (a i) (b i)i:ℕhac:c ≤ a ihbc:c ≤ b i⊢ measure (Ioo (a i) (b i) ∩ Ici c) + measure (Ioo (a i) (b i) \ Ici c) ≤ ENNReal.ofReal (b i - a i) have : Ioo (a i) (b i) ∩ Ici c = Ioo (a i) (b i) := c:ℝA:Set ℝa:ℕ → ℝb:ℕ → ℝh:A ⊆ ⋃ i, Ioo (a i) (b i)⊢ ∑' (i : ℕ), (measure (Ioo (a i) (b i) ∩ Ici c) + measure (Ioo (a i) (b i) \ Ici c)) ≤ ∑' (i : ℕ), ENNReal.ofReal (b i - a i) All goals completed! 🐙 c:ℝA:Set ℝa:ℕ → ℝb:ℕ → ℝh:A ⊆ ⋃ i, Ioo (a i) (b i)i:ℕhac:c ≤ a ihbc:c ≤ b ithis:Ioo (a i) (b i) ∩ Ici c = Ioo (a i) (b i) := isCaratheodory_Ici._proof_8 c a b i hac⊢ measure (Ioo (a i) (b i)) + measure (Ioo (a i) (b i) \ Ici c) ≤ ENNReal.ofReal (b i - a i) have : Ioo (a i) (b i) \ Ici c = ∅ := c:ℝA:Set ℝa:ℕ → ℝb:ℕ → ℝh:A ⊆ ⋃ i, Ioo (a i) (b i)⊢ ∑' (i : ℕ), (measure (Ioo (a i) (b i) ∩ Ici c) + measure (Ioo (a i) (b i) \ Ici c)) ≤ ∑' (i : ℕ), ENNReal.ofReal (b i - a i) All goals completed! 🐙 c:ℝA:Set ℝa:ℕ → ℝb:ℕ → ℝh:A ⊆ ⋃ i, Ioo (a i) (b i)i:ℕhac:c ≤ a ihbc:c ≤ b ithis✝:Ioo (a i) (b i) ∩ Ici c = Ioo (a i) (b i) := isCaratheodory_Ici._proof_8 c a b i hacthis:Ioo (a i) (b i) \ Ici c = ∅ := isCaratheodory_Ici._proof_9 c a b i hac⊢ measure (Ioo (a i) (b i)) + measure ∅ ≤ ENNReal.ofReal (b i - a i) c:ℝA:Set ℝa:ℕ → ℝb:ℕ → ℝh:A ⊆ ⋃ i, Ioo (a i) (b i)i:ℕhac:c ≤ a ihbc:c ≤ b ithis✝:Ioo (a i) (b i) ∩ Ici c = Ioo (a i) (b i) := isCaratheodory_Ici._proof_8 c a b i hacthis:Ioo (a i) (b i) \ Ici c = ∅ := isCaratheodory_Ici._proof_9 c a b i hac⊢ measure (Ioo (a i) (b i)) ≤ ENNReal.ofReal (b i - a i) All goals completed! 🐙
定理.

任意の可測集合はカラテオドリである。

Lean code
theorem MeasurableSet.isCaratheodory {A : Set ℝ} (h : MeasurableSet A) : IsCaratheodory A := A:Set ℝh:MeasurableSet A⊢ IsCaratheodory A induction h with A:Set ℝc:ℝ⊢ IsCaratheodory (Ici c) All goals completed! 🐙 A:Set ℝ⊢ IsCaratheodory ∅ All goals completed! 🐙 A✝:Set ℝA:Set ℝhA:MeasurableSet Aih:IsCaratheodory A⊢ IsCaratheodory Aᶜ All goals completed! 🐙 A✝:Set ℝA:ℕ → Set ℝhA:∀ (n : ℕ), MeasurableSet (A n)ih:∀ (n : ℕ), IsCaratheodory (A n)⊢ IsCaratheodory (⋃ i, A i) All goals completed! 🐙
定理.

A_1, A_2 \subseteq \mathbb{R} とする。 A_1 と A_2 が交わらず、A_1 が可測であると仮定する。 このとき m(A_1 \cup A_2) = m(A_1) + m(A_2) が成り立つ。

Lean code
theorem measure_union {A₁ A₂ : Set ℝ} (h : A₁ ∩ A₂ ⊆ ∅) (h₁ : MeasurableSet A₁) : measure (A₁ ∪ A₂) = measure (A₁) + measure (A₂) := measure_c_union h (h₁.isCaratheodory)
定理 (下からの連続性).

A_0, A_1, \dots \subset \mathbb{R} を可測集合の単調増大列とする。 このとき m(\bigcup_{n \in \mathbb{N}} A_n) = \sup_{n \in \mathbb{N}} m(A_n). が成り立つ。

Lean code
theorem measure_iUnion_of_monotone {A : ℕ → Set ℝ} (hA : Monotone A) : measure (⋃ i, A i) = ⨆ i, measure (A i) := A:ℕ → Set ℝhA:Monotone A⊢ measure (⋃ i, A i) = ⨆ i, measure (A i) A:ℕ → Set ℝhA:Monotone A⊢ measure (⋃ i, A i) ≤ ⨆ i, measure (A i) A:ℕ → Set ℝhA:Monotone AB:ℕ → Set ℝhAB:∀ (n : ℕ), A n ⊆ B nhBMeas:∀ (n : ℕ), MeasurableSet (B n)hBeq:∀ (n : ℕ), measure (B n) = measure (A n)⊢ measure (⋃ i, A i) ≤ ⨆ i, measure (A i) have hAC : ∀ n, A n ⊆ ⋂ i, B (n + i) := A:ℕ → Set ℝhA:Monotone A⊢ measure (⋃ i, A i) = ⨆ i, measure (A i) intro n A:ℕ → Set ℝhA:Monotone AB:ℕ → Set ℝhAB:∀ (n : ℕ), A n ⊆ B nhBMeas:∀ (n : ℕ), MeasurableSet (B n)hBeq:∀ (n : ℕ), measure (B n) = measure (A n)n:ℕx:ℝ⊢ x ∈ A n → x ∈ ⋂ i, B (n + i) A:ℕ → Set ℝhA:Monotone AB:ℕ → Set ℝhAB:∀ (n : ℕ), A n ⊆ B nhBMeas:∀ (n : ℕ), MeasurableSet (B n)hBeq:∀ (n : ℕ), measure (B n) = measure (A n)n:ℕx:ℝhx:x ∈ A n⊢ x ∈ ⋂ i, B (n + i) A:ℕ → Set ℝhA:Monotone AB:ℕ → Set ℝhAB:∀ (n : ℕ), A n ⊆ B nhBMeas:∀ (n : ℕ), MeasurableSet (B n)hBeq:∀ (n : ℕ), measure (B n) = measure (A n)n:ℕx:ℝhx:x ∈ A n⊢ ∀ (i : ℕ), x ∈ B (n + i) A:ℕ → Set ℝhA:Monotone AB:ℕ → Set ℝhAB:∀ (n : ℕ), A n ⊆ B nhBMeas:∀ (n : ℕ), MeasurableSet (B n)hBeq:∀ (n : ℕ), measure (B n) = measure (A n)n:ℕx:ℝhx:x ∈ A ni:ℕ⊢ x ∈ B (n + i) All goals completed! 🐙 have hCMeas : ∀ n, MeasurableSet (⋂ i, B (n + i)) := A:ℕ → Set ℝhA:Monotone A⊢ measure (⋃ i, A i) = ⨆ i, measure (A i) A:ℕ → Set ℝhA:Monotone AB:ℕ → Set ℝhAB:∀ (n : ℕ), A n ⊆ B nhBMeas:∀ (n : ℕ), MeasurableSet (B n)hBeq:∀ (n : ℕ), measure (B n) = measure (A n)hAC:∀ (n : ℕ), A n ⊆ ⋂ i, B (n + i) := fun n ⦃x⦄ hx => Eq.mpr (id measure_iUnion_of_monotone._simp_1) fun i => hAB (n + i) (hA (Nat.le_add_right n i) hx)n:ℕ⊢ MeasurableSet (⋂ i, B (n + i)) All goals completed! 🐙 have hCmono : Monotone (fun n ↦ ⋂ i, B (n + i)) := A:ℕ → Set ℝhA:Monotone A⊢ measure (⋃ i, A i) = ⨆ i, measure (A i) intro n A:ℕ → Set ℝhA:Monotone AB:ℕ → Set ℝhAB:∀ (n : ℕ), A n ⊆ B nhBMeas:∀ (n : ℕ), MeasurableSet (B n)hBeq:∀ (n : ℕ), measure (B n) = measure (A n)hAC:∀ (n : ℕ), A n ⊆ ⋂ i, B (n + i) := fun n ⦃x⦄ hx => Eq.mpr (id measure_iUnion_of_monotone._simp_1) fun i => hAB (n + i) (hA (Nat.le_add_right n i) hx)hCMeas:∀ (n : ℕ), MeasurableSet (⋂ i, B (n + i)) := fun n => MeasurableSet.iInter fun i => hBMeas (n + i)n:ℕm:ℕ⊢ n ≤ m → (fun n => ⋂ i, B (n + i)) n ≤ (fun n => ⋂ i, B (n + i)) m A:ℕ → Set ℝhA:Monotone AB:ℕ → Set ℝhAB:∀ (n : ℕ), A n ⊆ B nhBMeas:∀ (n : ℕ), MeasurableSet (B n)hBeq:∀ (n : ℕ), measure (B n) = measure (A n)hAC:∀ (n : ℕ), A n ⊆ ⋂ i, B (n + i) := fun n ⦃x⦄ hx => Eq.mpr (id measure_iUnion_of_monotone._simp_1) fun i => hAB (n + i) (hA (Nat.le_add_right n i) hx)hCMeas:∀ (n : ℕ), MeasurableSet (⋂ i, B (n + i)) := fun n => MeasurableSet.iInter fun i => hBMeas (n + i)n:ℕm:ℕhnm:n ≤ m⊢ (fun n => ⋂ i, B (n + i)) n ≤ (fun n => ⋂ i, B (n + i)) m A:ℕ → Set ℝhA:Monotone AB:ℕ → Set ℝhAB:∀ (n : ℕ), A n ⊆ B nhBMeas:∀ (n : ℕ), MeasurableSet (B n)hBeq:∀ (n : ℕ), measure (B n) = measure (A n)hAC:∀ (n : ℕ), A n ⊆ ⋂ i, B (n + i) := fun n ⦃x⦄ hx => Eq.mpr (id measure_iUnion_of_monotone._simp_1) fun i => hAB (n + i) (hA (Nat.le_add_right n i) hx)hCMeas:∀ (n : ℕ), MeasurableSet (⋂ i, B (n + i)) := fun n => MeasurableSet.iInter fun i => hBMeas (n + i)n:ℕm:ℕhnm:n ≤ mx:ℝ⊢ x ∈ (fun n => ⋂ i, B (n + i)) n → x ∈ (fun n => ⋂ i, B (n + i)) m A:ℕ → Set ℝhA:Monotone AB:ℕ → Set ℝhAB:∀ (n : ℕ), A n ⊆ B nhBMeas:∀ (n : ℕ), MeasurableSet (B n)hBeq:∀ (n : ℕ), measure (B n) = measure (A n)hAC:∀ (n : ℕ), A n ⊆ ⋂ i, B (n + i) := fun n ⦃x⦄ hx => Eq.mpr (id measure_iUnion_of_monotone._simp_1) fun i => hAB (n + i) (hA (Nat.le_add_right n i) hx)hCMeas:∀ (n : ℕ), MeasurableSet (⋂ i, B (n + i)) := fun n => MeasurableSet.iInter fun i => hBMeas (n + i)n:ℕm:ℕhnm:n ≤ mx:ℝhx:x ∈ (fun n => ⋂ i, B (n + i)) n⊢ x ∈ (fun n => ⋂ i, B (n + i)) m A:ℕ → Set ℝhA:Monotone AB:ℕ → Set ℝhAB:∀ (n : ℕ), A n ⊆ B nhBMeas:∀ (n : ℕ), MeasurableSet (B n)hBeq:∀ (n : ℕ), measure (B n) = measure (A n)hAC:∀ (n : ℕ), A n ⊆ ⋂ i, B (n + i) := fun n ⦃x⦄ hx => Eq.mpr (id measure_iUnion_of_monotone._simp_1) fun i => hAB (n + i) (hA (Nat.le_add_right n i) hx)hCMeas:∀ (n : ℕ), MeasurableSet (⋂ i, B (n + i)) := fun n => MeasurableSet.iInter fun i => hBMeas (n + i)n:ℕx:ℝhx:x ∈ (fun n => ⋂ i, B (n + i)) nk:ℕhnm:n ≤ n + k⊢ x ∈ (fun n => ⋂ i, B (n + i)) (n + k) A:ℕ → Set ℝhA:Monotone AB:ℕ → Set ℝhAB:∀ (n : ℕ), A n ⊆ B nhBMeas:∀ (n : ℕ), MeasurableSet (B n)hBeq:∀ (n : ℕ), measure (B n) = measure (A n)hAC:∀ (n : ℕ), A n ⊆ ⋂ i, B (n + i) := fun n ⦃x⦄ hx => Eq.mpr (id measure_iUnion_of_monotone._simp_1) fun i => hAB (n + i) (hA (Nat.le_add_right n i) hx)hCMeas:∀ (n : ℕ), MeasurableSet (⋂ i, B (n + i)) := fun n => MeasurableSet.iInter fun i => hBMeas (n + i)n:ℕx:ℝk:ℕhnm:n ≤ n + khx:∀ (i : ℕ), x ∈ B (n + i)⊢ ∀ (i : ℕ), x ∈ B (n + k + i) A:ℕ → Set ℝhA:Monotone AB:ℕ → Set ℝhAB:∀ (n : ℕ), A n ⊆ B nhBMeas:∀ (n : ℕ), MeasurableSet (B n)hBeq:∀ (n : ℕ), measure (B n) = measure (A n)hAC:∀ (n : ℕ), A n ⊆ ⋂ i, B (n + i) := fun n ⦃x⦄ hx => Eq.mpr (id measure_iUnion_of_monotone._simp_1) fun i => hAB (n + i) (hA (Nat.le_add_right n i) hx)hCMeas:∀ (n : ℕ), MeasurableSet (⋂ i, B (n + i)) := fun n => MeasurableSet.iInter fun i => hBMeas (n + i)n:ℕx:ℝk:ℕhnm:n ≤ n + khx:∀ (i : ℕ), x ∈ B (n + i)i:ℕ⊢ x ∈ B (n + k + i) All goals completed! 🐙 have hCeq : ∀ n, measure (⋂ i, B (n + i)) = measure (A n) := A:ℕ → Set ℝhA:Monotone A⊢ measure (⋃ i, A i) = ⨆ i, measure (A i) A:ℕ → Set ℝhA:Monotone AB:ℕ → Set ℝhAB:∀ (n : ℕ), A n ⊆ B nhBMeas:∀ (n : ℕ), MeasurableSet (B n)hBeq:∀ (n : ℕ), measure (B n) = measure (A n)hAC:∀ (n : ℕ), A n ⊆ ⋂ i, B (n + i) := fun n ⦃x⦄ hx => Eq.mpr (id measure_iUnion_of_monotone._simp_1) fun i => hAB (n + i) (hA (Nat.le_add_right n i) hx)hCMeas:∀ (n : ℕ), MeasurableSet (⋂ i, B (n + i)) := fun n => MeasurableSet.iInter fun i => hBMeas (n + i)hCmono:Monotone fun n => ⋂ i, B (n + i) := fun ⦃n m⦄ hnm ⦃x⦄ hx => Exists.casesOn (Nat.exists_eq_add_of_le hnm) fun k h => Eq.ndrec (motive := fun ⦃m⦄ => n ≤ m → x ∈ (fun n => ⋂ i, B (n + i)) m) (fun hnm => Eq.mpr (id measure_iUnion_of_monotone._simp_1) fun i => Eq.mpr (id (congrFun' (congrArg Membership.mem (congrArg B (Nat.add_assoc n k i))) x)) (Eq.mp measure_iUnion_of_monotone._simp_1 hx (k + i))) (Eq.symm h) hnmn:ℕ⊢ measure (⋂ i, B (n + i)) = measure (A n) have hsubset : ⋂ i, B (n + i) ⊆ B n := A:ℕ → Set ℝhA:Monotone A⊢ measure (⋃ i, A i) = ⨆ i, measure (A i) All goals completed! 🐙 A:ℕ → Set ℝhA:Monotone AB:ℕ → Set ℝhAB:∀ (n : ℕ), A n ⊆ B nhBMeas:∀ (n : ℕ), MeasurableSet (B n)hBeq:∀ (n : ℕ), measure (B n) = measure (A n)hAC:∀ (n : ℕ), A n ⊆ ⋂ i, B (n + i) := fun n ⦃x⦄ hx => Eq.mpr (id measure_iUnion_of_monotone._simp_1) fun i => hAB (n + i) (hA (Nat.le_add_right n i) hx)hCMeas:∀ (n : ℕ), MeasurableSet (⋂ i, B (n + i)) := fun n => MeasurableSet.iInter fun i => hBMeas (n + i)hCmono:Monotone fun n => ⋂ i, B (n + i) := fun ⦃n m⦄ hnm ⦃x⦄ hx => Exists.casesOn (Nat.exists_eq_add_of_le hnm) fun k h => Eq.ndrec (motive := fun ⦃m⦄ => n ≤ m → x ∈ (fun n => ⋂ i, B (n + i)) m) (fun hnm => Eq.mpr (id measure_iUnion_of_monotone._simp_1) fun i => Eq.mpr (id (congrFun' (congrArg Membership.mem (congrArg B (Nat.add_assoc n k i))) x)) (Eq.mp measure_iUnion_of_monotone._simp_1 hx (k + i))) (Eq.symm h) hnmn:ℕhsubset:⋂ i, B (n + i) ⊆ B n := Eq.mp (congrArg (Subset (⋂ i, B (n + i))) (congrArg B (add_zero n))) (iInter_subset (fun i => B (n + i)) 0)⊢ measure (⋂ i, B (n + i)) ≤ measure (A n) calc measure (⋂ i, B (n + i)) ≤ measure (B n) := measure_mono hsubset _ = measure (A n) := hBeq n calc measure (⋃ i, A i) ≤ measure (⋃ i, ⋂ j, B (i + j)) := measure_mono <| iUnion_mono hAC _ = ⨆ i, measure (⋂ j, B (i + j)) := measure_m_iUnion_of_monotone hCMeas hCmono _ = ⨆ i, measure (A i) := A:ℕ → Set ℝhA:Monotone AB:ℕ → Set ℝhAB:∀ (n : ℕ), A n ⊆ B nhBMeas:∀ (n : ℕ), MeasurableSet (B n)hBeq:∀ (n : ℕ), measure (B n) = measure (A n)hAC:∀ (n : ℕ), A n ⊆ ⋂ i, B (n + i) := fun n ⦃x⦄ hx => Eq.mpr (id measure_iUnion_of_monotone._simp_1) fun i => hAB (n + i) (hA (Nat.le_add_right n i) hx)hCMeas:∀ (n : ℕ), MeasurableSet (⋂ i, B (n + i)) := fun n => MeasurableSet.iInter fun i => hBMeas (n + i)hCmono:Monotone fun n => ⋂ i, B (n + i) := fun ⦃n m⦄ hnm ⦃x⦄ hx => Exists.casesOn (Nat.exists_eq_add_of_le hnm) fun k h => Eq.ndrec (motive := fun ⦃m⦄ => n ≤ m → x ∈ (fun n => ⋂ i, B (n + i)) m) (fun hnm => Eq.mpr (id measure_iUnion_of_monotone._simp_1) fun i => Eq.mpr (id (congrFun' (congrArg Membership.mem (congrArg B (Nat.add_assoc n k i))) x)) (Eq.mp measure_iUnion_of_monotone._simp_1 hx (k + i))) (Eq.symm h) hnmhCeq:∀ (n : ℕ), measure (⋂ i, B (n + i)) = measure (A n) := fun n => have hsubset := Eq.mp (congrArg (Subset (⋂ i, B (n + i))) (congrArg B (add_zero n))) (iInter_subset (fun i => B (n + i)) 0); le_antisymm (Trans.trans (measure_mono hsubset) (hBeq n)) (measure_mono (hAC n))⊢ ⨆ i, measure (⋂ j, B (i + j)) = ⨆ i, measure (A i) All goals completed! 🐙
定理 (可算加法性).

A_0, A_1, \dots \subset \mathbb{R} を互いに交わらない可測集合の列とする。 このとき m(\bigcup_{n \in \mathbb{N}} A_n) = \sum_{n \in \mathbb{N}} m(A_n). が成り立つ。

Lean code
theorem measure_iUnion (A : ℕ → Set ℝ) (hA : ∀ n, MeasurableSet (A n)) (hdA : Pairwise (Disjoint on A)) : measure (⋃ n, A n) = ∑' n, measure (A n) := measure_c_iUnion A (fun n ↦ (hA n).isCaratheodory) hdA