2.1. 実数直線上の測度
定義 (ルベーグ外測度).
集合 A \subseteq \mathbb{R} の ルベーグ外測度 を次で定義する:
m (A) \coloneqq
\inf_{a : \mathbb{N} \to \mathbb{R},\, b : \mathbb{N} \to \mathbb{R},\,
A \subseteq \bigcup_{n} (a_n, b_n)}
\sum_{n \in \mathbb{N}} (b_n - a_n)^+ \ \in \ [0, \infty].
ここで、x \in \mathbb{R} に対して x^+ \coloneqq \max(x, 0) \in [0, \infty] とする。
Lean code
def measure (A : Set ℝ) : ℝ≥0∞ :=
⨅ (a : ℕ → ℝ) (b : ℕ → ℝ) (_ : A ⊆ ⋃ i, Ioo (a i) (b i)), ∑' i, .ofReal (b i - a i)
補題.
A \subseteq \bigcup_{i \in \mathbb{N}} (a_i, b_i) ならば、
m (A) \le \sum_{n \in \mathbb{N}} (b_n - a_n)^+ が成り立つ。
Lean code
theorem measure_le (A : Set ℝ) (a b : ℕ → ℝ)
(hA : A ⊆ ⋃ i, Ioo (a i) (b i)) :
measure A ≤ ∑' i, .ofReal (b i - a i) :=
iInf₂_le_of_le a b (iInf_le_of_le hA (le_of_eq rfl))
定理 (区間の測度は長さに等しい).
任意の a, b \in \mathbb{R} に対して、m([a,b]) = (b-a)^+ が成り立つ。
Lean code
theorem measure_Icc_le (a b : ℝ) :
measure (Icc a b) ≤ .ofReal (b - a) := a:ℝb:ℝ⊢ measure (Icc a b) ≤ ENNReal.ofReal (b - a)
a:ℝb:ℝ⊢ ∀ (ε : NNReal), 0 < ε → ENNReal.ofReal (b - a) < ∞ → measure (Icc a b) ≤ ENNReal.ofReal (b - a) + ↑ε
intro ε a:ℝb:ℝε:NNRealhε:0 < ε⊢ ENNReal.ofReal (b - a) < ∞ → measure (Icc a b) ≤ ENNReal.ofReal (b - a) + ↑ε a:ℝb:ℝε:NNRealhε:0 < εhab':ENNReal.ofReal (b - a) < ∞⊢ measure (Icc a b) ≤ ENNReal.ofReal (b - a) + ↑ε
a:ℝb:ℝε:NNRealhε:0 < εhab':ENNReal.ofReal (b - a) < ∞a':ℕ → ℝ :=
fun x =>
match x with
| 0 => a - ↑ε / 2
| n.succ => 0⊢ measure (Icc a b) ≤ ENNReal.ofReal (b - a) + ↑ε
a:ℝb:ℝε:NNRealhε:0 < εhab':ENNReal.ofReal (b - a) < ∞a':ℕ → ℝ :=
fun x =>
match x with
| 0 => a - ↑ε / 2
| n.succ => 0b':ℕ → ℝ :=
fun x =>
match x with
| 0 => b + ↑ε / 2
| n.succ => 0⊢ measure (Icc a b) ≤ ENNReal.ofReal (b - a) + ↑ε
have ha : a - ε / 2 < a := a:ℝb:ℝ⊢ measure (Icc a b) ≤ ENNReal.ofReal (b - a)
a:ℝb:ℝε:NNRealhε:0 < εhab':ENNReal.ofReal (b - a) < ∞a':ℕ → ℝ :=
fun x =>
match x with
| 0 => a - ↑ε / 2
| n.succ => 0b':ℕ → ℝ :=
fun x =>
match x with
| 0 => b + ↑ε / 2
| n.succ => 0⊢ 0 < ↑ε / 2
All goals completed! 🐙
have hb : b < b + ε / 2 := a:ℝb:ℝ⊢ measure (Icc a b) ≤ ENNReal.ofReal (b - a)
a:ℝb:ℝε:NNRealhε:0 < εhab':ENNReal.ofReal (b - a) < ∞a':ℕ → ℝ :=
fun x =>
match x with
| 0 => a - ↑ε / 2
| n.succ => 0b':ℕ → ℝ :=
fun x =>
match x with
| 0 => b + ↑ε / 2
| n.succ => 0ha:a - ↑ε / 2 < a := Eq.mpr (id (congrArg (fun _a => _a) (propext (sub_lt_self_iff a)))) (half_pos hε)⊢ 0 < ↑ε / 2
All goals completed! 🐙
have :=
calc
Icc a b
_ ⊆ Ioo (a - ε / 2) (b + ε / 2) := Icc_subset_Ioo (a:ℝb:ℝε:NNRealhε:0 < εhab':ENNReal.ofReal (b - a) < ∞a':ℕ → ℝ :=
fun x =>
match x with
| 0 => a - ↑ε / 2
| n.succ => 0b':ℕ → ℝ :=
fun x =>
match x with
| 0 => b + ↑ε / 2
| n.succ => 0ha:a - ↑ε / 2 < a := Eq.mpr (id (congrArg (fun _a => _a) (propext (sub_lt_self_iff a)))) (half_pos hε)hb:b < b + ↑ε / 2 := Eq.mpr (id (congrArg (fun _a => _a) (propext (lt_add_iff_pos_right b)))) (half_pos hε)⊢ a - ↑ε / 2 < a All goals completed! 🐙) (a:ℝb:ℝε:NNRealhε:0 < εhab':ENNReal.ofReal (b - a) < ∞a':ℕ → ℝ :=
fun x =>
match x with
| 0 => a - ↑ε / 2
| n.succ => 0b':ℕ → ℝ :=
fun x =>
match x with
| 0 => b + ↑ε / 2
| n.succ => 0ha:a - ↑ε / 2 < a := Eq.mpr (id (congrArg (fun _a => _a) (propext (sub_lt_self_iff a)))) (half_pos hε)hb:b < b + ↑ε / 2 := Eq.mpr (id (congrArg (fun _a => _a) (propext (lt_add_iff_pos_right b)))) (half_pos hε)⊢ b < b + ↑ε / 2 All goals completed! 🐙)
_ ⊆ ⋃ i, Ioo (a' i) (b' i) := subset_iUnion_of_subset 0 (subset_refl _)
a:ℝb:ℝε:NNRealhε:0 < εhab':ENNReal.ofReal (b - a) < ∞a':ℕ → ℝ :=
fun x =>
match x with
| 0 => a - ↑ε / 2
| n.succ => 0b':ℕ → ℝ :=
fun x =>
match x with
| 0 => b + ↑ε / 2
| n.succ => 0ha:a - ↑ε / 2 < a := Eq.mpr (id (congrArg (fun _a => _a) (propext (sub_lt_self_iff a)))) (half_pos hε)hb:b < b + ↑ε / 2 := Eq.mpr (id (congrArg (fun _a => _a) (propext (lt_add_iff_pos_right b)))) (half_pos hε)this✝:Icc a b ⊆ ⋃ i, Ioo (a' i) (b' i) :=
Trans.trans (Trans.trans rfl (Icc_subset_Ioo (measure_Icc_le._proof_3 a ε ha) (measure_Icc_le._proof_4 b ε hb)))
(subset_iUnion_of_subset 0 (subset_refl (Ioo (a - ↑ε / 2) (b + ↑ε / 2))))this:measure (Icc a b) ≤ ∑' (i : ℕ), ENNReal.ofReal (b' i - a' i) := measure_le (Icc a b) a' b' this✝⊢ measure (Icc a b) ≤ ENNReal.ofReal (b - a) + ↑ε
a:ℝb:ℝε:NNRealhε:0 < εhab':ENNReal.ofReal (b - a) < ∞a':ℕ → ℝ :=
fun x =>
match x with
| 0 => a - ↑ε / 2
| n.succ => 0b':ℕ → ℝ :=
fun x =>
match x with
| 0 => b + ↑ε / 2
| n.succ => 0ha:a - ↑ε / 2 < a := Eq.mpr (id (congrArg (fun _a => _a) (propext (sub_lt_self_iff a)))) (half_pos hε)hb:b < b + ↑ε / 2 := Eq.mpr (id (congrArg (fun _a => _a) (propext (lt_add_iff_pos_right b)))) (half_pos hε)this✝:Icc a b ⊆ ⋃ i, Ioo (a' i) (b' i) :=
Trans.trans (Trans.trans rfl (Icc_subset_Ioo (measure_Icc_le._proof_3 a ε ha) (measure_Icc_le._proof_4 b ε hb)))
(subset_iUnion_of_subset 0 (subset_refl (Ioo (a - ↑ε / 2) (b + ↑ε / 2))))this:measure (Icc a b) ≤ ENNReal.ofReal (b' 0 - a' 0)⊢ measure (Icc a b) ≤ ENNReal.ofReal (b - a) + ↑εa:ℝb:ℝε:NNRealhε:0 < εhab':ENNReal.ofReal (b - a) < ∞a':ℕ → ℝ :=
fun x =>
match x with
| 0 => a - ↑ε / 2
| n.succ => 0b':ℕ → ℝ :=
fun x =>
match x with
| 0 => b + ↑ε / 2
| n.succ => 0ha:a - ↑ε / 2 < a := Eq.mpr (id (congrArg (fun _a => _a) (propext (sub_lt_self_iff a)))) (half_pos hε)hb:b < b + ↑ε / 2 := Eq.mpr (id (congrArg (fun _a => _a) (propext (lt_add_iff_pos_right b)))) (half_pos hε)this✝:Icc a b ⊆ ⋃ i, Ioo (a' i) (b' i) :=
Trans.trans (Trans.trans rfl (Icc_subset_Ioo (measure_Icc_le._proof_3 a ε ha) (measure_Icc_le._proof_4 b ε hb)))
(subset_iUnion_of_subset 0 (subset_refl (Ioo (a - ↑ε / 2) (b + ↑ε / 2))))this:measure (Icc a b) ≤ ∑' (i : ℕ), ENNReal.ofReal (b' i - a' i) := measure_le (Icc a b) a' b' this✝⊢ ∀ (b'_1 : ℕ), b'_1 ≠ 0 → ENNReal.ofReal (b' b'_1 - a' b'_1) = 0
a:ℝb:ℝε:NNRealhε:0 < εhab':ENNReal.ofReal (b - a) < ∞a':ℕ → ℝ :=
fun x =>
match x with
| 0 => a - ↑ε / 2
| n.succ => 0b':ℕ → ℝ :=
fun x =>
match x with
| 0 => b + ↑ε / 2
| n.succ => 0ha:a - ↑ε / 2 < a := Eq.mpr (id (congrArg (fun _a => _a) (propext (sub_lt_self_iff a)))) (half_pos hε)hb:b < b + ↑ε / 2 := Eq.mpr (id (congrArg (fun _a => _a) (propext (lt_add_iff_pos_right b)))) (half_pos hε)this✝:Icc a b ⊆ ⋃ i, Ioo (a' i) (b' i) :=
Trans.trans (Trans.trans rfl (Icc_subset_Ioo (measure_Icc_le._proof_3 a ε ha) (measure_Icc_le._proof_4 b ε hb)))
(subset_iUnion_of_subset 0 (subset_refl (Ioo (a - ↑ε / 2) (b + ↑ε / 2))))this:measure (Icc a b) ≤ ENNReal.ofReal (b' 0 - a' 0)⊢ measure (Icc a b) ≤ ENNReal.ofReal (b - a) + ↑ε calc
measure (Icc a b)
_ ≤ ENNReal.ofReal (b' 0 - a' 0) := this
_ = ENNReal.ofReal (b - a + ε) := a:ℝb:ℝε:NNRealhε:0 < εhab':ENNReal.ofReal (b - a) < ∞a':ℕ → ℝ :=
fun x =>
match x with
| 0 => a - ↑ε / 2
| n.succ => 0b':ℕ → ℝ :=
fun x =>
match x with
| 0 => b + ↑ε / 2
| n.succ => 0ha:a - ↑ε / 2 < a := Eq.mpr (id (congrArg (fun _a => _a) (propext (sub_lt_self_iff a)))) (half_pos hε)hb:b < b + ↑ε / 2 := Eq.mpr (id (congrArg (fun _a => _a) (propext (lt_add_iff_pos_right b)))) (half_pos hε)this✝:Icc a b ⊆ ⋃ i, Ioo (a' i) (b' i) :=
Trans.trans (Trans.trans rfl (Icc_subset_Ioo (measure_Icc_le._proof_3 a ε ha) (measure_Icc_le._proof_4 b ε hb)))
(subset_iUnion_of_subset 0 (subset_refl (Ioo (a - ↑ε / 2) (b + ↑ε / 2))))this:measure (Icc a b) ≤ ENNReal.ofReal (b' 0 - a' 0)⊢ ENNReal.ofReal (b' 0 - a' 0) = ENNReal.ofReal (b - a + ↑ε) All goals completed! 🐙
_ ≤ ENNReal.ofReal (b - a) + ENNReal.ofReal ε := ENNReal.ofReal_add_le
_ = ENNReal.ofReal (b - a) + ε := a:ℝb:ℝε:NNRealhε:0 < εhab':ENNReal.ofReal (b - a) < ∞a':ℕ → ℝ :=
fun x =>
match x with
| 0 => a - ↑ε / 2
| n.succ => 0b':ℕ → ℝ :=
fun x =>
match x with
| 0 => b + ↑ε / 2
| n.succ => 0ha:a - ↑ε / 2 < a := Eq.mpr (id (congrArg (fun _a => _a) (propext (sub_lt_self_iff a)))) (half_pos hε)hb:b < b + ↑ε / 2 := Eq.mpr (id (congrArg (fun _a => _a) (propext (lt_add_iff_pos_right b)))) (half_pos hε)this✝:Icc a b ⊆ ⋃ i, Ioo (a' i) (b' i) :=
Trans.trans (Trans.trans rfl (Icc_subset_Ioo (measure_Icc_le._proof_3 a ε ha) (measure_Icc_le._proof_4 b ε hb)))
(subset_iUnion_of_subset 0 (subset_refl (Ioo (a - ↑ε / 2) (b + ↑ε / 2))))this:measure (Icc a b) ≤ ENNReal.ofReal (b' 0 - a' 0)⊢ ENNReal.ofReal (b - a) + ENNReal.ofReal ↑ε = ENNReal.ofReal (b - a) + ↑ε All goals completed! 🐙
a:ℝb:ℝε:NNRealhε:0 < εhab':ENNReal.ofReal (b - a) < ∞a':ℕ → ℝ :=
fun x =>
match x with
| 0 => a - ↑ε / 2
| n.succ => 0b':ℕ → ℝ :=
fun x =>
match x with
| 0 => b + ↑ε / 2
| n.succ => 0ha:a - ↑ε / 2 < a := Eq.mpr (id (congrArg (fun _a => _a) (propext (sub_lt_self_iff a)))) (half_pos hε)hb:b < b + ↑ε / 2 := Eq.mpr (id (congrArg (fun _a => _a) (propext (lt_add_iff_pos_right b)))) (half_pos hε)this✝:Icc a b ⊆ ⋃ i, Ioo (a' i) (b' i) :=
Trans.trans (Trans.trans rfl (Icc_subset_Ioo (measure_Icc_le._proof_3 a ε ha) (measure_Icc_le._proof_4 b ε hb)))
(subset_iUnion_of_subset 0 (subset_refl (Ioo (a - ↑ε / 2) (b + ↑ε / 2))))this:measure (Icc a b) ≤ ∑' (i : ℕ), ENNReal.ofReal (b' i - a' i) := measure_le (Icc a b) a' b' this✝⊢ ∀ (b'_1 : ℕ), b'_1 ≠ 0 → ENNReal.ofReal (b' b'_1 - a' b'_1) = 0 intro n a:ℝb:ℝε:NNRealhε:0 < εhab':ENNReal.ofReal (b - a) < ∞a':ℕ → ℝ :=
fun x =>
match x with
| 0 => a - ↑ε / 2
| n.succ => 0b':ℕ → ℝ :=
fun x =>
match x with
| 0 => b + ↑ε / 2
| n.succ => 0ha:a - ↑ε / 2 < a := Eq.mpr (id (congrArg (fun _a => _a) (propext (sub_lt_self_iff a)))) (half_pos hε)hb:b < b + ↑ε / 2 := Eq.mpr (id (congrArg (fun _a => _a) (propext (lt_add_iff_pos_right b)))) (half_pos hε)this✝:Icc a b ⊆ ⋃ i, Ioo (a' i) (b' i) :=
Trans.trans (Trans.trans rfl (Icc_subset_Ioo (measure_Icc_le._proof_3 a ε ha) (measure_Icc_le._proof_4 b ε hb)))
(subset_iUnion_of_subset 0 (subset_refl (Ioo (a - ↑ε / 2) (b + ↑ε / 2))))this:measure (Icc a b) ≤ ∑' (i : ℕ), ENNReal.ofReal (b' i - a' i) := measure_le (Icc a b) a' b' this✝n:ℕhn:n ≠ 0⊢ ENNReal.ofReal (b' n - a' n) = 0
have ha'n : a' n = 0 := a:ℝb:ℝ⊢ measure (Icc a b) ≤ ENNReal.ofReal (b - a)
cases n with
a:ℝb:ℝε:NNRealhε:0 < εhab':ENNReal.ofReal (b - a) < ∞a':ℕ → ℝ :=
fun x =>
match x with
| 0 => a - ↑ε / 2
| n.succ => 0b':ℕ → ℝ :=
fun x =>
match x with
| 0 => b + ↑ε / 2
| n.succ => 0ha:a - ↑ε / 2 < a := Eq.mpr (id (congrArg (fun _a => _a) (propext (sub_lt_self_iff a)))) (half_pos hε)hb:b < b + ↑ε / 2 := Eq.mpr (id (congrArg (fun _a => _a) (propext (lt_add_iff_pos_right b)))) (half_pos hε)this✝:Icc a b ⊆ ⋃ i, Ioo (a' i) (b' i) :=
Trans.trans (Trans.trans rfl (Icc_subset_Ioo (measure_Icc_le._proof_3 a ε ha) (measure_Icc_le._proof_4 b ε hb)))
(subset_iUnion_of_subset 0 (subset_refl (Ioo (a - ↑ε / 2) (b + ↑ε / 2))))this:measure (Icc a b) ≤ ∑' (i : ℕ), ENNReal.ofReal (b' i - a' i) := measure_le (Icc a b) a' b' this✝hn:0 ≠ 0⊢ a' 0 = 0 All goals completed! 🐙
a:ℝb:ℝε:NNRealhε:0 < εhab':ENNReal.ofReal (b - a) < ∞a':ℕ → ℝ :=
fun x =>
match x with
| 0 => a - ↑ε / 2
| n.succ => 0b':ℕ → ℝ :=
fun x =>
match x with
| 0 => b + ↑ε / 2
| n.succ => 0ha:a - ↑ε / 2 < a := Eq.mpr (id (congrArg (fun _a => _a) (propext (sub_lt_self_iff a)))) (half_pos hε)hb:b < b + ↑ε / 2 := Eq.mpr (id (congrArg (fun _a => _a) (propext (lt_add_iff_pos_right b)))) (half_pos hε)this✝:Icc a b ⊆ ⋃ i, Ioo (a' i) (b' i) :=
Trans.trans (Trans.trans rfl (Icc_subset_Ioo (measure_Icc_le._proof_3 a ε ha) (measure_Icc_le._proof_4 b ε hb)))
(subset_iUnion_of_subset 0 (subset_refl (Ioo (a - ↑ε / 2) (b + ↑ε / 2))))this:measure (Icc a b) ≤ ∑' (i : ℕ), ENNReal.ofReal (b' i - a' i) := measure_le (Icc a b) a' b' this✝n✝:ℕhn:n✝ + 1 ≠ 0⊢ a' (n✝ + 1) = 0 All goals completed! 🐙
have hb'n : b' n = 0 := a:ℝb:ℝ⊢ measure (Icc a b) ≤ ENNReal.ofReal (b - a)
cases n with
a:ℝb:ℝε:NNRealhε:0 < εhab':ENNReal.ofReal (b - a) < ∞a':ℕ → ℝ :=
fun x =>
match x with
| 0 => a - ↑ε / 2
| n.succ => 0b':ℕ → ℝ :=
fun x =>
match x with
| 0 => b + ↑ε / 2
| n.succ => 0ha:a - ↑ε / 2 < a := Eq.mpr (id (congrArg (fun _a => _a) (propext (sub_lt_self_iff a)))) (half_pos hε)hb:b < b + ↑ε / 2 := Eq.mpr (id (congrArg (fun _a => _a) (propext (lt_add_iff_pos_right b)))) (half_pos hε)this✝:Icc a b ⊆ ⋃ i, Ioo (a' i) (b' i) :=
Trans.trans (Trans.trans rfl (Icc_subset_Ioo (measure_Icc_le._proof_3 a ε ha) (measure_Icc_le._proof_4 b ε hb)))
(subset_iUnion_of_subset 0 (subset_refl (Ioo (a - ↑ε / 2) (b + ↑ε / 2))))this:measure (Icc a b) ≤ ∑' (i : ℕ), ENNReal.ofReal (b' i - a' i) := measure_le (Icc a b) a' b' this✝hn:0 ≠ 0ha'n:a' 0 = 0⊢ b' 0 = 0 All goals completed! 🐙
a:ℝb:ℝε:NNRealhε:0 < εhab':ENNReal.ofReal (b - a) < ∞a':ℕ → ℝ :=
fun x =>
match x with
| 0 => a - ↑ε / 2
| n.succ => 0b':ℕ → ℝ :=
fun x =>
match x with
| 0 => b + ↑ε / 2
| n.succ => 0ha:a - ↑ε / 2 < a := Eq.mpr (id (congrArg (fun _a => _a) (propext (sub_lt_self_iff a)))) (half_pos hε)hb:b < b + ↑ε / 2 := Eq.mpr (id (congrArg (fun _a => _a) (propext (lt_add_iff_pos_right b)))) (half_pos hε)this✝:Icc a b ⊆ ⋃ i, Ioo (a' i) (b' i) :=
Trans.trans (Trans.trans rfl (Icc_subset_Ioo (measure_Icc_le._proof_3 a ε ha) (measure_Icc_le._proof_4 b ε hb)))
(subset_iUnion_of_subset 0 (subset_refl (Ioo (a - ↑ε / 2) (b + ↑ε / 2))))this:measure (Icc a b) ≤ ∑' (i : ℕ), ENNReal.ofReal (b' i - a' i) := measure_le (Icc a b) a' b' this✝n✝:ℕhn:n✝ + 1 ≠ 0ha'n:a' (n✝ + 1) = 0⊢ b' (n✝ + 1) = 0 All goals completed! 🐙
All goals completed! 🐙theorem measure_Icc (a b : ℝ) : measure (Icc a b) = .ofReal (b - a) := a:ℝb:ℝ⊢ measure (Icc a b) = ENNReal.ofReal (b - a)
a:ℝb:ℝ⊢ ENNReal.ofReal (b - a) ≤ measure (Icc a b)
a:ℝb:ℝa':ℕ → ℝb':ℕ → ℝhab:Icc a b ⊆ ⋃ i, Ioo (a' i) (b' i)⊢ ENNReal.ofReal (b - a) ≤ ∑' (i : ℕ), ENNReal.ofReal (b' i - a' i)
suffices
∀ (s : Finset ℕ) (a b), Icc a b ⊆ (⋃ i ∈ (s : Set ℕ), Ioo (a' i) (b' i)) →
(.ofReal (b - a) : ℝ≥0∞) ≤ ∑ i ∈ s, .ofReal ((b' i) - (a' i)) a:ℝb:ℝa':ℕ → ℝb':ℕ → ℝhab:Icc a b ⊆ ⋃ i, Ioo (a' i) (b' i)this:∀ (s : Finset ℕ) (a b : ℝ),
Icc a b ⊆ ⋃ i ∈ ↑s, Ioo (a' i) (b' i) → ENNReal.ofReal (b - a) ≤ ∑ i ∈ s, ENNReal.ofReal (b' i - a' i) :=
?m.78⊢ ENNReal.ofReal (b - a) ≤ ∑' (i : ℕ), ENNReal.ofReal (b' i - a' i)
rcases isCompact_Icc.elim_finite_subcover_image
(fun (i : ℕ) (_ : i ∈ univ) ↦ isOpen_Ioo) (a:ℝb:ℝa':ℕ → ℝb':ℕ → ℝhab:Icc a b ⊆ ⋃ i, Ioo (a' i) (b' i)this:∀ (s : Finset ℕ) (a b : ℝ),
Icc a b ⊆ ⋃ i ∈ ↑s, Ioo (a' i) (b' i) → ENNReal.ofReal (b - a) ≤ ∑ i ∈ s, ENNReal.ofReal (b' i - a' i) :=
?m.78⊢ Icc ?m.85 ?m.86 ⊆ ⋃ i ∈ univ, Ioo (?m.109 i) (?m.110 i) All goals completed! 🐙) with
⟨s, _, hf, hs⟩
have e :
⋃ i ∈ (hf.toFinset : Set ℕ), Ioo (a' i) (b' i) = ⋃ i ∈ s, Ioo (a' i) (b' i) := a:ℝb:ℝa':ℕ → ℝb':ℕ → ℝhab:Icc a b ⊆ ⋃ i, Ioo (a' i) (b' i)this:∀ (s : Finset ℕ) (a b : ℝ),
Icc a b ⊆ ⋃ i ∈ ↑s, Ioo (a' i) (b' i) → ENNReal.ofReal (b - a) ≤ ∑ i ∈ s, ENNReal.ofReal (b' i - a' i) :=
?m.78⊢ ENNReal.ofReal (b - a) ≤ ∑' (i : ℕ), ENNReal.ofReal (b' i - a' i)
All goals completed! 🐙
a:ℝb:ℝa':ℕ → ℝb':ℕ → ℝhab:Icc a b ⊆ ⋃ i, Ioo (a' i) (b' i)this:∀ (s : Finset ℕ) (a b : ℝ),
Icc a b ⊆ ⋃ i ∈ ↑s, Ioo (a' i) (b' i) → ENNReal.ofReal (b - a) ≤ ∑ i ∈ s, ENNReal.ofReal (b' i - a' i) :=
?m.78s:Set ℕleft✝:s ⊆ univhf:s.Finitehs:Icc a b ⊆ ⋃ i ∈ s, Ioo (a' i) (b' i)e:⋃ i ∈ ↑hf.toFinset, Ioo (a' i) (b' i) = ⋃ i ∈ s, Ioo (a' i) (b' i) :=
of_eq_true
(Eq.trans
(congrFun'
(congrArg Eq
(congrArg iUnion
(funext fun x =>
iUnion_congr_Prop (Iff.of_eq (measure_Icc._simp_1 hf)) fun x_1 => Eq.refl (Ioo (a' x) (b' x)))))
(⋃ x ∈ s, Ioo (a' x) (b' x)))
(eq_self (⋃ x ∈ s, Ioo (a' x) (b' x))))⊢ ENNReal.ofReal (b - a) ≤ ⨆ s, ∑ a ∈ s, ENNReal.ofReal (b' a - a' a)
a:ℝb:ℝa':ℕ → ℝb':ℕ → ℝhab:Icc a b ⊆ ⋃ i, Ioo (a' i) (b' i)this:∀ (s : Finset ℕ) (a b : ℝ),
Icc a b ⊆ ⋃ i ∈ ↑s, Ioo (a' i) (b' i) → ENNReal.ofReal (b - a) ≤ ∑ i ∈ s, ENNReal.ofReal (b' i - a' i) :=
?m.78s:Set ℕleft✝:s ⊆ univhf:s.Finitehs:Icc a b ⊆ ⋃ i ∈ s, Ioo (a' i) (b' i)e:⋃ i ∈ ↑hf.toFinset, Ioo (a' i) (b' i) = ⋃ i ∈ s, Ioo (a' i) (b' i) :=
of_eq_true
(Eq.trans
(congrFun'
(congrArg Eq
(congrArg iUnion
(funext fun x =>
iUnion_congr_Prop (Iff.of_eq (measure_Icc._simp_1 hf)) fun x_1 => Eq.refl (Ioo (a' x) (b' x)))))
(⋃ x ∈ s, Ioo (a' x) (b' x)))
(eq_self (⋃ x ∈ s, Ioo (a' x) (b' x))))⊢ ENNReal.ofReal (b - a) ≤ ∑ a ∈ hf.toFinset, ENNReal.ofReal (b' a - a' a)
apply this hf.toFinset _ _ (a:ℝb:ℝa':ℕ → ℝb':ℕ → ℝhab:Icc a b ⊆ ⋃ i, Ioo (a' i) (b' i)this:∀ (s : Finset ℕ) (a b : ℝ),
Icc a b ⊆ ⋃ i ∈ ↑s, Ioo (a' i) (b' i) → ENNReal.ofReal (b - a) ≤ ∑ i ∈ s, ENNReal.ofReal (b' i - a' i) :=
?m.78s:Set ℕleft✝:s ⊆ univhf:s.Finitehs:Icc a b ⊆ ⋃ i ∈ s, Ioo (a' i) (b' i)e:⋃ i ∈ ↑hf.toFinset, Ioo (a' i) (b' i) = ⋃ i ∈ s, Ioo (a' i) (b' i) :=
of_eq_true
(Eq.trans
(congrFun'
(congrArg Eq
(congrArg iUnion
(funext fun x =>
iUnion_congr_Prop (Iff.of_eq (measure_Icc._simp_1 hf)) fun x_1 => Eq.refl (Ioo (a' x) (b' x)))))
(⋃ x ∈ s, Ioo (a' x) (b' x)))
(eq_self (⋃ x ∈ s, Ioo (a' x) (b' x))))⊢ Icc a b ⊆ ⋃ i ∈ ↑hf.toFinset, Ioo (a' i) (b' i) All goals completed! 🐙)
a:ℝa':ℕ → ℝb':ℕ → ℝ⊢ ∀ (s : Finset ℕ) (a b : ℝ),
Icc a b ⊆ ⋃ i ∈ ↑s, Ioo (a' i) (b' i) → ENNReal.ofReal (b - a) ≤ ∑ i ∈ s, ENNReal.ofReal (b' i - a' i)
a✝:ℝa':ℕ → ℝb':ℕ → ℝs✝:Finset ℕs:Finset ℕIH:∀ t ⊂ s,
∀ (a b : ℝ), Icc a b ⊆ ⋃ i ∈ ↑t, Ioo (a' i) (b' i) → ENNReal.ofReal (b - a) ≤ ∑ i ∈ t, ENNReal.ofReal (b' i - a' i)a:ℝb:ℝh:Icc a b ⊆ ⋃ i ∈ ↑s, Ioo (a' i) (b' i)⊢ ENNReal.ofReal (b - a) ≤ ∑ i ∈ s, ENNReal.ofReal (b' i - a' i)
a✝:ℝa':ℕ → ℝb':ℕ → ℝs✝:Finset ℕs:Finset ℕIH:∀ t ⊂ s,
∀ (a b : ℝ), Icc a b ⊆ ⋃ i ∈ ↑t, Ioo (a' i) (b' i) → ENNReal.ofReal (b - a) ≤ ∑ i ∈ t, ENNReal.ofReal (b' i - a' i)a:ℝb:ℝh:Icc a b ⊆ ⋃ i ∈ ↑s, Ioo (a' i) (b' i)hab':a > b⊢ ENNReal.ofReal (b - a) ≤ ∑ i ∈ s, ENNReal.ofReal (b' i - a' i)a✝:ℝa':ℕ → ℝb':ℕ → ℝs✝:Finset ℕs:Finset ℕIH:∀ t ⊂ s,
∀ (a b : ℝ), Icc a b ⊆ ⋃ i ∈ ↑t, Ioo (a' i) (b' i) → ENNReal.ofReal (b - a) ≤ ∑ i ∈ t, ENNReal.ofReal (b' i - a' i)a:ℝb:ℝh:Icc a b ⊆ ⋃ i ∈ ↑s, Ioo (a' i) (b' i)hab':¬a > b⊢ ENNReal.ofReal (b - a) ≤ ∑ i ∈ s, ENNReal.ofReal (b' i - a' i)
a✝:ℝa':ℕ → ℝb':ℕ → ℝs✝:Finset ℕs:Finset ℕIH:∀ t ⊂ s,
∀ (a b : ℝ), Icc a b ⊆ ⋃ i ∈ ↑t, Ioo (a' i) (b' i) → ENNReal.ofReal (b - a) ≤ ∑ i ∈ t, ENNReal.ofReal (b' i - a' i)a:ℝb:ℝh:Icc a b ⊆ ⋃ i ∈ ↑s, Ioo (a' i) (b' i)hab':a > b⊢ ENNReal.ofReal (b - a) ≤ ∑ i ∈ s, ENNReal.ofReal (b' i - a' i) have : b - a ≤ 0 := a:ℝb:ℝ⊢ measure (Icc a b) = ENNReal.ofReal (b - a) All goals completed! 🐙
a✝:ℝa':ℕ → ℝb':ℕ → ℝs✝:Finset ℕs:Finset ℕIH:∀ t ⊂ s,
∀ (a b : ℝ), Icc a b ⊆ ⋃ i ∈ ↑t, Ioo (a' i) (b' i) → ENNReal.ofReal (b - a) ≤ ∑ i ∈ t, ENNReal.ofReal (b' i - a' i)a:ℝb:ℝh:Icc a b ⊆ ⋃ i ∈ ↑s, Ioo (a' i) (b' i)hab':a > bthis:b - a ≤ 0 := measure_Icc._proof_1 a b hab'⊢ 0 ≤ ∑ i ∈ s, ENNReal.ofReal (b' i - a' i)
All goals completed! 🐙
a✝:ℝa':ℕ → ℝb':ℕ → ℝs✝:Finset ℕs:Finset ℕIH:∀ t ⊂ s,
∀ (a b : ℝ), Icc a b ⊆ ⋃ i ∈ ↑t, Ioo (a' i) (b' i) → ENNReal.ofReal (b - a) ≤ ∑ i ∈ t, ENNReal.ofReal (b' i - a' i)a:ℝb:ℝh:Icc a b ⊆ ⋃ i ∈ ↑s, Ioo (a' i) (b' i)hab':¬a > ba_le_b:a ≤ b := le_of_not_gt hab'⊢ ENNReal.ofReal (b - a) ≤ ∑ i ∈ s, ENNReal.ofReal (b' i - a' i)
a✝:ℝa':ℕ → ℝb':ℕ → ℝs✝:Finset ℕs:Finset ℕIH:∀ t ⊂ s,
∀ (a b : ℝ), Icc a b ⊆ ⋃ i ∈ ↑t, Ioo (a' i) (b' i) → ENNReal.ofReal (b - a) ≤ ∑ i ∈ t, ENNReal.ofReal (b' i - a' i)a:ℝb:ℝh:Icc a b ⊆ ⋃ i ∈ ↑s, Ioo (a' i) (b' i)hab':¬a > ba_le_b:a ≤ b := le_of_not_gt hab'this:b ∈ ⋃ i ∈ ↑s, Ioo (a' i) (b' i) := h ⟨a_le_b, le_rfl⟩⊢ ENNReal.ofReal (b - a) ≤ ∑ i ∈ s, ENNReal.ofReal (b' i - a' i)
a✝:ℝa':ℕ → ℝb':ℕ → ℝs✝:Finset ℕs:Finset ℕIH:∀ t ⊂ s,
∀ (a b : ℝ), Icc a b ⊆ ⋃ i ∈ ↑t, Ioo (a' i) (b' i) → ENNReal.ofReal (b - a) ≤ ∑ i ∈ t, ENNReal.ofReal (b' i - a' i)a:ℝb:ℝh:Icc a b ⊆ ⋃ i ∈ ↑s, Ioo (a' i) (b' i)hab':¬a > ba_le_b:a ≤ b := le_of_not_gt hab'this:∃ i, a' i < b ∧ i ∈ s ∧ b < b' i⊢ ENNReal.ofReal (b - a) ≤ ∑ i ∈ s, ENNReal.ofReal (b' i - a' i)
a✝:ℝa':ℕ → ℝb':ℕ → ℝs✝:Finset ℕs:Finset ℕIH:∀ t ⊂ s,
∀ (a b : ℝ), Icc a b ⊆ ⋃ i ∈ ↑t, Ioo (a' i) (b' i) → ENNReal.ofReal (b - a) ≤ ∑ i ∈ t, ENNReal.ofReal (b' i - a' i)a:ℝb:ℝh:Icc a b ⊆ ⋃ i ∈ ↑s, Ioo (a' i) (b' i)hab':¬a > ba_le_b:a ≤ b := le_of_not_gt hab'i:ℕcb:a' i < bis:i ∈ sbd:b < b' i⊢ ENNReal.ofReal (b - a) ≤ ∑ i ∈ s, ENNReal.ofReal (b' i - a' i)
a✝:ℝa':ℕ → ℝb':ℕ → ℝs✝:Finset ℕs:Finset ℕIH:∀ t ⊂ s,
∀ (a b : ℝ), Icc a b ⊆ ⋃ i ∈ ↑t, Ioo (a' i) (b' i) → ENNReal.ofReal (b - a) ≤ ∑ i ∈ t, ENNReal.ofReal (b' i - a' i)a:ℝb:ℝhab':¬a > ba_le_b:a ≤ b := le_of_not_gt hab'i:ℕh:Icc a b ⊆ ⋃ i_1 ∈ ↑(insert i (s.erase i)), Ioo (a' i_1) (b' i_1)cb:a' i < bis:i ∈ sbd:b < b' i⊢ ENNReal.ofReal (b - a) ≤ ∑ i ∈ insert i (s.erase i), ENNReal.ofReal (b' i - a' i)
a✝:ℝa':ℕ → ℝb':ℕ → ℝs✝:Finset ℕs:Finset ℕIH:∀ t ⊂ s,
∀ (a b : ℝ), Icc a b ⊆ ⋃ i ∈ ↑t, Ioo (a' i) (b' i) → ENNReal.ofReal (b - a) ≤ ∑ i ∈ t, ENNReal.ofReal (b' i - a' i)a:ℝb:ℝhab':¬a > ba_le_b:a ≤ b := le_of_not_gt hab'i:ℕh:Icc a b ⊆ Ioo (a' i) (b' i) ∪ ⋃ x ∈ ↑(s.erase i), Ioo (a' x) (b' x)cb:a' i < bis:i ∈ sbd:b < b' i⊢ ENNReal.ofReal (b - a) ≤ ∑ i ∈ insert i (s.erase i), ENNReal.ofReal (b' i - a' i)
a✝:ℝa':ℕ → ℝb':ℕ → ℝs✝:Finset ℕs:Finset ℕIH:∀ t ⊂ s,
∀ (a b : ℝ), Icc a b ⊆ ⋃ i ∈ ↑t, Ioo (a' i) (b' i) → ENNReal.ofReal (b - a) ≤ ∑ i ∈ t, ENNReal.ofReal (b' i - a' i)a:ℝb:ℝhab':¬a > ba_le_b:a ≤ b := le_of_not_gt hab'i:ℕh:Icc a b ⊆ Ioo (a' i) (b' i) ∪ ⋃ x ∈ ↑(s.erase i), Ioo (a' x) (b' x)cb:a' i < bis:i ∈ sbd:b < b' i⊢ ENNReal.ofReal (b - a) ≤ ENNReal.ofReal (b' i - a' i) + ∑ x ∈ s.erase i, ENNReal.ofReal (b' x - a' x)
grw [← IH _ (Finset.erase_ssubset is) a (a' i), ← ENNReal.ofReal_add_lea✝:ℝa':ℕ → ℝb':ℕ → ℝs✝:Finset ℕs:Finset ℕIH:∀ t ⊂ s,
∀ (a b : ℝ), Icc a b ⊆ ⋃ i ∈ ↑t, Ioo (a' i) (b' i) → ENNReal.ofReal (b - a) ≤ ∑ i ∈ t, ENNReal.ofReal (b' i - a' i)a:ℝb:ℝhab':¬a > ba_le_b:a ≤ b := le_of_not_gt hab'i:ℕh:Icc a b ⊆ Ioo (a' i) (b' i) ∪ ⋃ x ∈ ↑(s.erase i), Ioo (a' x) (b' x)cb:a' i < bis:i ∈ sbd:b < b' i⊢ ENNReal.ofReal (b - a) ≤ ENNReal.ofReal (b' i - a' i + (a' i - a))a✝:ℝa':ℕ → ℝb':ℕ → ℝs✝:Finset ℕs:Finset ℕIH:∀ t ⊂ s,
∀ (a b : ℝ), Icc a b ⊆ ⋃ i ∈ ↑t, Ioo (a' i) (b' i) → ENNReal.ofReal (b - a) ≤ ∑ i ∈ t, ENNReal.ofReal (b' i - a' i)a:ℝb:ℝhab':¬a > ba_le_b:a ≤ b := le_of_not_gt hab'i:ℕh:Icc a b ⊆ Ioo (a' i) (b' i) ∪ ⋃ x ∈ ↑(s.erase i), Ioo (a' x) (b' x)cb:a' i < bis:i ∈ sbd:b < b' i⊢ Icc a (a' i) ⊆ ⋃ i_1 ∈ ↑(s.erase i), Ioo (a' i_1) (b' i_1)
a✝:ℝa':ℕ → ℝb':ℕ → ℝs✝:Finset ℕs:Finset ℕIH:∀ t ⊂ s,
∀ (a b : ℝ), Icc a b ⊆ ⋃ i ∈ ↑t, Ioo (a' i) (b' i) → ENNReal.ofReal (b - a) ≤ ∑ i ∈ t, ENNReal.ofReal (b' i - a' i)a:ℝb:ℝhab':¬a > ba_le_b:a ≤ b := le_of_not_gt hab'i:ℕh:Icc a b ⊆ Ioo (a' i) (b' i) ∪ ⋃ x ∈ ↑(s.erase i), Ioo (a' x) (b' x)cb:a' i < bis:i ∈ sbd:b < b' i⊢ ENNReal.ofReal (b - a) ≤ ENNReal.ofReal (b' i - a' i + (a' i - a)) a✝:ℝa':ℕ → ℝb':ℕ → ℝs✝:Finset ℕs:Finset ℕIH:∀ t ⊂ s,
∀ (a b : ℝ), Icc a b ⊆ ⋃ i ∈ ↑t, Ioo (a' i) (b' i) → ENNReal.ofReal (b - a) ≤ ∑ i ∈ t, ENNReal.ofReal (b' i - a' i)a:ℝb:ℝhab':¬a > ba_le_b:a ≤ b := le_of_not_gt hab'i:ℕh:Icc a b ⊆ Ioo (a' i) (b' i) ∪ ⋃ x ∈ ↑(s.erase i), Ioo (a' x) (b' x)cb:a' i < bis:i ∈ sbd:b < b' i⊢ b - a ≤ b' i - a' i + (a' i - a)
a✝:ℝa':ℕ → ℝb':ℕ → ℝs✝:Finset ℕs:Finset ℕIH:∀ t ⊂ s,
∀ (a b : ℝ), Icc a b ⊆ ⋃ i ∈ ↑t, Ioo (a' i) (b' i) → ENNReal.ofReal (b - a) ≤ ∑ i ∈ t, ENNReal.ofReal (b' i - a' i)a:ℝb:ℝhab':¬a > ba_le_b:a ≤ b := le_of_not_gt hab'i:ℕh:Icc a b ⊆ Ioo (a' i) (b' i) ∪ ⋃ x ∈ ↑(s.erase i), Ioo (a' x) (b' x)cb:a' i < bis:i ∈ sbd:b < b' i⊢ b - a ≤ b' i - a
All goals completed! 🐙
a✝:ℝa':ℕ → ℝb':ℕ → ℝs✝:Finset ℕs:Finset ℕIH:∀ t ⊂ s,
∀ (a b : ℝ), Icc a b ⊆ ⋃ i ∈ ↑t, Ioo (a' i) (b' i) → ENNReal.ofReal (b - a) ≤ ∑ i ∈ t, ENNReal.ofReal (b' i - a' i)a:ℝb:ℝhab':¬a > ba_le_b:a ≤ b := le_of_not_gt hab'i:ℕh:Icc a b ⊆ Ioo (a' i) (b' i) ∪ ⋃ x ∈ ↑(s.erase i), Ioo (a' x) (b' x)cb:a' i < bis:i ∈ sbd:b < b' i⊢ Icc a (a' i) ⊆ ⋃ i_1 ∈ ↑(s.erase i), Ioo (a' i_1) (b' i_1) a✝:ℝa':ℕ → ℝb':ℕ → ℝs✝:Finset ℕs:Finset ℕIH:∀ t ⊂ s,
∀ (a b : ℝ), Icc a b ⊆ ⋃ i ∈ ↑t, Ioo (a' i) (b' i) → ENNReal.ofReal (b - a) ≤ ∑ i ∈ t, ENNReal.ofReal (b' i - a' i)a:ℝb:ℝhab':¬a > ba_le_b:a ≤ b := le_of_not_gt hab'i:ℕh:Icc a b ⊆ Ioo (a' i) (b' i) ∪ ⋃ x ∈ ↑(s.erase i), Ioo (a' x) (b' x)cb:a' i < bis:i ∈ sbd:b < b' ix:ℝh₁:a ≤ xh₂:x ≤ a' i⊢ x ∈ ⋃ i_1 ∈ ↑(s.erase i), Ioo (a' i_1) (b' i_1)
All goals completed! 🐙
補題.
-
m(\emptyset) = 0である。 -
A, B \subseteq \mathbb{R}がA \subseteq Bを満たすなら、m(A) \leq m(B)が成り立つ。 -
A_0, A_1, \dots \subseteq \mathbb{R}に対して、m\left( \bigcup_{n \in \mathbb{N}} A_n \right) \leq \sum_{n \in \mathbb{N}} m(A_n).が成り立つ。
Lean code
@[simp]
theorem measure_empty : measure (∅ : Set ℝ) = 0 := ⊢ measure ∅ = 0
simpa using measure_le ∅ 0 0 (⊢ ∅ ⊆ ⋃ i, Ioo (0 i) (0 i) All goals completed! 🐙)@[grind →]
theorem measure_mono {A B : Set ℝ} (h : A ⊆ B) :
measure A ≤ measure B :=
iInf₂_mono fun _a _b ↦ iInf_const_mono fun hA ↦ h.trans hAtheorem measure_iUnion_le (A : ℕ → Set ℝ) :
measure (⋃ n, A n) ≤ ∑' n, measure (A n) := A:ℕ → Set ℝ⊢ measure (⋃ n, A n) ≤ ∑' (n : ℕ), measure (A n)
A:ℕ → Set ℝ⊢ ∀ (ε : NNReal), 0 < ε → ∑' (n : ℕ), measure (A n) < ∞ → measure (⋃ n, A n) ≤ ∑' (n : ℕ), measure (A n) + ↑ε
intro ε A:ℕ → Set ℝε:NNRealhε:0 < ε⊢ ∑' (n : ℕ), measure (A n) < ∞ → measure (⋃ n, A n) ≤ ∑' (n : ℕ), measure (A n) + ↑ε A:ℕ → Set ℝε:NNRealhε:0 < εhb:∑' (n : ℕ), measure (A n) < ∞⊢ measure (⋃ n, A n) ≤ ∑' (n : ℕ), measure (A n) + ↑ε
A:ℕ → Set ℝε:NNRealhε:0 < εhb:∑' (n : ℕ), measure (A n) < ∞ε':ℕ → NNRealhε':∀ (i : ℕ), 0 < ε' ihl:∑' (i : ℕ), ↑(ε' i) < ↑ε⊢ measure (⋃ n, A n) ≤ ∑' (n : ℕ), measure (A n) + ↑ε
A:ℕ → Set ℝε:NNRealhε:0 < εhb:∑' (n : ℕ), measure (A n) < ∞ε':ℕ → NNRealhε':∀ (i : ℕ), 0 < ε' ihl:∑' (i : ℕ), ↑(ε' i) < ↑ε⊢ measure (⋃ n, A n) ≤ ∑' (n : ℕ), measure (A n) + ∑' (i : ℕ), ↑(ε' i)
A:ℕ → Set ℝε:NNRealhε:0 < εhb:∑' (n : ℕ), measure (A n) < ∞ε':ℕ → NNRealhε':∀ (i : ℕ), 0 < ε' ihl:∑' (i : ℕ), ↑(ε' i) < ↑ε⊢ measure (⋃ n, A n) ≤ ∑' (a : ℕ), (measure (A a) + ↑(ε' a))
choose a b hab using
show ∀ i, ∃ a : ℕ → ℝ, ∃ b : ℕ → ℝ, (A i ⊆ ⋃ i, Ioo (a i) (b i)) ∧
(∑' i, ENNReal.ofReal (b i - a i)) < measure (A i) + ε' i A:ℕ → Set ℝ⊢ measure (⋃ n, A n) ≤ ∑' (n : ℕ), measure (A n)
A:ℕ → Set ℝε:NNRealhε:0 < εhb:∑' (n : ℕ), measure (A n) < ∞ε':ℕ → NNRealhε':∀ (i : ℕ), 0 < ε' ihl:∑' (i : ℕ), ↑(ε' i) < ↑εi:ℕ⊢ ∃ a b, A i ⊆ ⋃ i, Ioo (a i) (b i) ∧ ∑' (i : ℕ), ENNReal.ofReal (b i - a i) < measure (A i) + ↑(ε' i)
have : measure (A i) < measure (A i) + ε' i :=
ENNReal.lt_add_right (ne_top_of_le_ne_top hb.ne <| ENNReal.le_tsum _)
(A:ℕ → Set ℝε:NNRealhε:0 < εhb:∑' (n : ℕ), measure (A n) < ∞ε':ℕ → NNRealhε':∀ (i : ℕ), 0 < ε' ihl:∑' (i : ℕ), ↑(ε' i) < ↑εi:ℕ⊢ ↑(ε' i) ≠ 0 All goals completed! 🐙)
A:ℕ → Set ℝε:NNRealhε:0 < εhb:∑' (n : ℕ), measure (A n) < ∞ε':ℕ → NNRealhε':∀ (i : ℕ), 0 < ε' ihl:∑' (i : ℕ), ↑(ε' i) < ↑εi:ℕthis:measure (A i) < measure (A i) + ↑(ε' i) :=
lt_add_right (ne_top_of_le_ne_top (LT.lt.ne hb) (ENNReal.le_tsum i))
(Eq.mpr (id (congrArg Not coe_eq_zero._simp_1)) (LT.lt.ne' (hε' i)))a:ℕ → ℝht:⨅ b, ⨅ (_ : A i ⊆ ⋃ i, Ioo (a i) (b i)), ∑' (i : ℕ), ENNReal.ofReal (b i - a i) < measure (A i) + ↑(ε' i)⊢ ∃ a b, A i ⊆ ⋃ i, Ioo (a i) (b i) ∧ ∑' (i : ℕ), ENNReal.ofReal (b i - a i) < measure (A i) + ↑(ε' i)
A:ℕ → Set ℝε:NNRealhε:0 < εhb:∑' (n : ℕ), measure (A n) < ∞ε':ℕ → NNRealhε':∀ (i : ℕ), 0 < ε' ihl:∑' (i : ℕ), ↑(ε' i) < ↑εi:ℕthis:measure (A i) < measure (A i) + ↑(ε' i) :=
lt_add_right (ne_top_of_le_ne_top (LT.lt.ne hb) (ENNReal.le_tsum i))
(Eq.mpr (id (congrArg Not coe_eq_zero._simp_1)) (LT.lt.ne' (hε' i)))a:ℕ → ℝht:⨅ b, ⨅ (_ : A i ⊆ ⋃ i, Ioo (a i) (b i)), ∑' (i : ℕ), ENNReal.ofReal (b i - a i) < measure (A i) + ↑(ε' i)b:ℕ → ℝht':⨅ (_ : A i ⊆ ⋃ i, Ioo (a i) (b i)), ∑' (i : ℕ), ENNReal.ofReal (b i - a i) < measure (A i) + ↑(ε' i)⊢ ∃ a b, A i ⊆ ⋃ i, Ioo (a i) (b i) ∧ ∑' (i : ℕ), ENNReal.ofReal (b i - a i) < measure (A i) + ↑(ε' i)
A:ℕ → Set ℝε:NNRealhε:0 < εhb:∑' (n : ℕ), measure (A n) < ∞ε':ℕ → NNRealhε':∀ (i : ℕ), 0 < ε' ihl:∑' (i : ℕ), ↑(ε' i) < ↑εi:ℕthis:measure (A i) < measure (A i) + ↑(ε' i) :=
lt_add_right (ne_top_of_le_ne_top (LT.lt.ne hb) (ENNReal.le_tsum i))
(Eq.mpr (id (congrArg Not coe_eq_zero._simp_1)) (LT.lt.ne' (hε' i)))a:ℕ → ℝht:⨅ b, ⨅ (_ : A i ⊆ ⋃ i, Ioo (a i) (b i)), ∑' (i : ℕ), ENNReal.ofReal (b i - a i) < measure (A i) + ↑(ε' i)b:ℕ → ℝht':⨅ (_ : A i ⊆ ⋃ i, Ioo (a i) (b i)), ∑' (i : ℕ), ENNReal.ofReal (b i - a i) < measure (A i) + ↑(ε' i)hab:A i ⊆ ⋃ i, Ioo (a i) (b i)h:∑' (i : ℕ), ENNReal.ofReal (b i - a i) < measure (A i) + ↑(ε' i)⊢ ∃ a b, A i ⊆ ⋃ i, Ioo (a i) (b i) ∧ ∑' (i : ℕ), ENNReal.ofReal (b i - a i) < measure (A i) + ↑(ε' i)
All goals completed! 🐙
A:ℕ → Set ℝε:NNRealhε:0 < εhb:∑' (n : ℕ), measure (A n) < ∞ε':ℕ → NNRealhε':∀ (i : ℕ), 0 < ε' ihl:∑' (i : ℕ), ↑(ε' i) < ↑εa:ℕ → ℕ → ℝb:ℕ → ℕ → ℝhab✝:∀ (i : ℕ),
A i ⊆ ⋃ i_1, Ioo (a i i_1) (b i i_1) ∧ ∑' (i_1 : ℕ), ENNReal.ofReal (b i i_1 - a i i_1) < measure (A i) + ↑(ε' i)hab:∀ (i : ℕ), A i ⊆ ⋃ j, Ioo (a i j) (b i j) ∧ ∑' (j : ℕ), ENNReal.ofReal (b i j - a i j) < measure (A i) + ↑(ε' i) := hab✝⊢ measure (⋃ n, A n) ≤ ∑' (a : ℕ), (measure (A a) + ↑(ε' a))
A:ℕ → Set ℝε:NNRealhε:0 < εhb:∑' (n : ℕ), measure (A n) < ∞ε':ℕ → NNRealhε':∀ (i : ℕ), 0 < ε' ihl:∑' (i : ℕ), ↑(ε' i) < ↑εa:ℕ → ℕ → ℝb:ℕ → ℕ → ℝhab✝:∀ (i : ℕ),
A i ⊆ ⋃ i_1, Ioo (a i i_1) (b i i_1) ∧ ∑' (i_1 : ℕ), ENNReal.ofReal (b i i_1 - a i i_1) < measure (A i) + ↑(ε' i)hab:∀ (i : ℕ), A i ⊆ ⋃ j, Ioo (a i j) (b i j) ∧ ∑' (j : ℕ), ENNReal.ofReal (b i j - a i j) < measure (A i) + ↑(ε' i) := hab✝⊢ measure (⋃ n, A n) ≤ ∑' (a_1 : ℕ) (j : ℕ), ENNReal.ofReal (b a_1 j - a a_1 j)
A:ℕ → Set ℝε:NNRealhε:0 < εhb:∑' (n : ℕ), measure (A n) < ∞ε':ℕ → NNRealhε':∀ (i : ℕ), 0 < ε' ihl:∑' (i : ℕ), ↑(ε' i) < ↑εa:ℕ → ℕ → ℝb:ℕ → ℕ → ℝhab✝:∀ (i : ℕ),
A i ⊆ ⋃ i_1, Ioo (a i i_1) (b i i_1) ∧ ∑' (i_1 : ℕ), ENNReal.ofReal (b i i_1 - a i i_1) < measure (A i) + ↑(ε' i)hab:∀ (i : ℕ), A i ⊆ ⋃ j, Ioo (a i j) (b i j) ∧ ∑' (j : ℕ), ENNReal.ofReal (b i j - a i j) < measure (A i) + ↑(ε' i) := hab✝⊢ measure (⋃ n, A n) ≤
∑' (c : ℕ),
ENNReal.ofReal
(b (Nat.pairEquiv.symm c).1 (Nat.pairEquiv.symm c).2 - a (Nat.pairEquiv.symm c).1 (Nat.pairEquiv.symm c).2)
A:ℕ → Set ℝε:NNRealhε:0 < εhb:∑' (n : ℕ), measure (A n) < ∞ε':ℕ → NNRealhε':∀ (i : ℕ), 0 < ε' ihl:∑' (i : ℕ), ↑(ε' i) < ↑εa:ℕ → ℕ → ℝb:ℕ → ℕ → ℝhab✝:∀ (i : ℕ),
A i ⊆ ⋃ i_1, Ioo (a i i_1) (b i i_1) ∧ ∑' (i_1 : ℕ), ENNReal.ofReal (b i i_1 - a i i_1) < measure (A i) + ↑(ε' i)hab:∀ (i : ℕ), A i ⊆ ⋃ j, Ioo (a i j) (b i j) ∧ ∑' (j : ℕ), ENNReal.ofReal (b i j - a i j) < measure (A i) + ↑(ε' i) := hab✝⊢ measure (⋃ n, A n) ≤
∑' (c : ℕ), ENNReal.ofReal (b (Nat.unpair c).1 (Nat.unpair c).2 - a (Nat.unpair c).1 (Nat.unpair c).2)
A:ℕ → Set ℝε:NNRealhε:0 < εhb:∑' (n : ℕ), measure (A n) < ∞ε':ℕ → NNRealhε':∀ (i : ℕ), 0 < ε' ihl:∑' (i : ℕ), ↑(ε' i) < ↑εa:ℕ → ℕ → ℝb:ℕ → ℕ → ℝhab✝:∀ (i : ℕ),
A i ⊆ ⋃ i_1, Ioo (a i i_1) (b i i_1) ∧ ∑' (i_1 : ℕ), ENNReal.ofReal (b i i_1 - a i i_1) < measure (A i) + ↑(ε' i)hab:∀ (i : ℕ), A i ⊆ ⋃ j, Ioo (a i j) (b i j) ∧ ∑' (j : ℕ), ENNReal.ofReal (b i j - a i j) < measure (A i) + ↑(ε' i) := hab✝⊢ ∑' (i : ℕ), ENNReal.ofReal (b (Nat.unpair i).1 (Nat.unpair i).2 - a (Nat.unpair i).1 (Nat.unpair i).2) ≤
∑' (c : ℕ), ENNReal.ofReal (b (Nat.unpair c).1 (Nat.unpair c).2 - a (Nat.unpair c).1 (Nat.unpair c).2)A:ℕ → Set ℝε:NNRealhε:0 < εhb:∑' (n : ℕ), measure (A n) < ∞ε':ℕ → NNRealhε':∀ (i : ℕ), 0 < ε' ihl:∑' (i : ℕ), ↑(ε' i) < ↑εa:ℕ → ℕ → ℝb:ℕ → ℕ → ℝhab✝:∀ (i : ℕ),
A i ⊆ ⋃ i_1, Ioo (a i i_1) (b i i_1) ∧ ∑' (i_1 : ℕ), ENNReal.ofReal (b i i_1 - a i i_1) < measure (A i) + ↑(ε' i)hab:∀ (i : ℕ), A i ⊆ ⋃ j, Ioo (a i j) (b i j) ∧ ∑' (j : ℕ), ENNReal.ofReal (b i j - a i j) < measure (A i) + ↑(ε' i) := hab✝⊢ ⋃ n, A n ⊆
⋃ i, Ioo ((fun i => a (Nat.unpair i).1 (Nat.unpair i).2) i) ((fun i => b (Nat.unpair i).1 (Nat.unpair i).2) i)
A:ℕ → Set ℝε:NNRealhε:0 < εhb:∑' (n : ℕ), measure (A n) < ∞ε':ℕ → NNRealhε':∀ (i : ℕ), 0 < ε' ihl:∑' (i : ℕ), ↑(ε' i) < ↑εa:ℕ → ℕ → ℝb:ℕ → ℕ → ℝhab✝:∀ (i : ℕ),
A i ⊆ ⋃ i_1, Ioo (a i i_1) (b i i_1) ∧ ∑' (i_1 : ℕ), ENNReal.ofReal (b i i_1 - a i i_1) < measure (A i) + ↑(ε' i)hab:∀ (i : ℕ), A i ⊆ ⋃ j, Ioo (a i j) (b i j) ∧ ∑' (j : ℕ), ENNReal.ofReal (b i j - a i j) < measure (A i) + ↑(ε' i) := hab✝⊢ ∑' (i : ℕ), ENNReal.ofReal (b (Nat.unpair i).1 (Nat.unpair i).2 - a (Nat.unpair i).1 (Nat.unpair i).2) ≤
∑' (c : ℕ), ENNReal.ofReal (b (Nat.unpair c).1 (Nat.unpair c).2 - a (Nat.unpair c).1 (Nat.unpair c).2) All goals completed! 🐙
A:ℕ → Set ℝε:NNRealhε:0 < εhb:∑' (n : ℕ), measure (A n) < ∞ε':ℕ → NNRealhε':∀ (i : ℕ), 0 < ε' ihl:∑' (i : ℕ), ↑(ε' i) < ↑εa:ℕ → ℕ → ℝb:ℕ → ℕ → ℝhab✝:∀ (i : ℕ),
A i ⊆ ⋃ i_1, Ioo (a i i_1) (b i i_1) ∧ ∑' (i_1 : ℕ), ENNReal.ofReal (b i i_1 - a i i_1) < measure (A i) + ↑(ε' i)hab:∀ (i : ℕ), A i ⊆ ⋃ j, Ioo (a i j) (b i j) ∧ ∑' (j : ℕ), ENNReal.ofReal (b i j - a i j) < measure (A i) + ↑(ε' i) := hab✝i:ℕj:ℕ⊢ Ioo (a i j) (b i j) ⊆
⋃ i, Ioo ((fun i => a (Nat.unpair i).1 (Nat.unpair i).2) i) ((fun i => b (Nat.unpair i).1 (Nat.unpair i).2) i)
A:ℕ → Set ℝε:NNRealhε:0 < εhb:∑' (n : ℕ), measure (A n) < ∞ε':ℕ → NNRealhε':∀ (i : ℕ), 0 < ε' ihl:∑' (i : ℕ), ↑(ε' i) < ↑εa:ℕ → ℕ → ℝb:ℕ → ℕ → ℝhab✝:∀ (i : ℕ),
A i ⊆ ⋃ i_1, Ioo (a i i_1) (b i i_1) ∧ ∑' (i_1 : ℕ), ENNReal.ofReal (b i i_1 - a i i_1) < measure (A i) + ↑(ε' i)hab:∀ (i : ℕ), A i ⊆ ⋃ j, Ioo (a i j) (b i j) ∧ ∑' (j : ℕ), ENNReal.ofReal (b i j - a i j) < measure (A i) + ↑(ε' i) := hab✝i:ℕj:ℕ⊢ Ioo (a i j) (b i j) ⊆ ⋃ i, ⋃ j, Ioo (a i j) (b i j)
All goals completed! 🐙