α : Type u_1
β : Type ?u.15791
R : Type ?u.15794
R' : Type ?u.15797
ms : Set (OuterMeasure α)
m✝ m : OuterMeasure α
s : ℕ → Set α
h_mono : ∀ (n : ℕ), s n ⊆ s (n + 1)
h0 : (∑' (k : ℕ), ↑m (s (k + 1) \ s k)) ≠ ⊤
inst✝ : (i : ℕ) → DecidablePred fun x => x ∈ s i
⊢ Tendsto (fun k => ↑m ((⋃ (n : ℕ), s n) \ s k)) atTop (𝓝 0)
α : Type u_1
β : Type ?u.15791
R : Type ?u.15794
R' : Type ?u.15797
ms : Set (OuterMeasure α)
m✝ m : OuterMeasure α
s : ℕ → Set α
h_mono : ∀ (n : ℕ), s n ⊆ s (n + 1)
h0 : (∑' (k : ℕ), ↑m (s (k + 1) \ s k)) ≠ ⊤
inst✝ : (i : ℕ) → DecidablePred fun x => x ∈ s i
⊢ ↑m (⋃ (n : ℕ), s n) = ⨆ (n : ℕ), ↑m (s n)
refine' m.iUnion_of_tendsto_zero atTop _
α : Type u_1
β : Type ?u.15791
R : Type ?u.15794
R' : Type ?u.15797
ms : Set (OuterMeasure α)
m✝ m : OuterMeasure α
s : ℕ → Set α
h_mono : ∀ (n : ℕ), s n ⊆ s (n + 1)
h0 : (∑' (k : ℕ), ↑m (s (k + 1) \ s k)) ≠ ⊤
inst✝ : (i : ℕ) → DecidablePred fun x => x ∈ s i
n : ℕ
⊢ ↑m ((⋃ (n : ℕ), s n) \ s n) ≤ ∑' (k : ℕ), ↑m (s (k + n + 1) \ s (k + n))
α : Type u_1
β : Type ?u.15791
R : Type ?u.15794
R' : Type ?u.15797
ms : Set (OuterMeasure α)
m✝ m : OuterMeasure α
s : ℕ → Set α
h_mono : ∀ (n : ℕ), s n ⊆ s (n + 1)
h0 : (∑' (k : ℕ), ↑m (s (k + 1) \ s k)) ≠ ⊤
inst✝ : (i : ℕ) → DecidablePred fun x => x ∈ s i
⊢ Tendsto (fun k => ↑m ((⋃ (n : ℕ), s n) \ s k)) atTop (𝓝 0)
refine' tendsto_nhds_bot_mono' (ENNReal.tendsto_sum_nat_add _ h0) fun n => _
α : Type u_1
β : Type ?u.15791
R : Type ?u.15794
R' : Type ?u.15797
ms : Set (OuterMeasure α)
m✝ m : OuterMeasure α
s : ℕ → Set α
h_mono : ∀ (n : ℕ), s n ⊆ s (n + 1)
h0 : (∑' (k : ℕ), ↑m (s (k + 1) \ s k)) ≠ ⊤
inst✝ : (i : ℕ) → DecidablePred fun x => x ∈ s i
n : ℕ
⊢ (⋃ (n : ℕ), s n) \ s n ⊆ ⋃ (i : ℕ), s (i + n + 1) \ s (i + n)
α : Type u_1
β : Type ?u.15791
R : Type ?u.15794
R' : Type ?u.15797
ms : Set (OuterMeasure α)
m✝ m : OuterMeasure α
s : ℕ → Set α
h_mono : ∀ (n : ℕ), s n ⊆ s (n + 1)
h0 : (∑' (k : ℕ), ↑m (s (k + 1) \ s k)) ≠ ⊤
inst✝ : (i : ℕ) → DecidablePred fun x => x ∈ s i
n : ℕ
⊢ ↑m ((⋃ (n : ℕ), s n) \ s n) ≤ ∑' (k : ℕ), ↑m (s (k + n + 1) \ s (k + n))
refine' (m.mono _).trans (m.iUnion _)
α : Type u_1
β : Type ?u.15791
R : Type ?u.15794
R' : Type ?u.15797
ms : Set (OuterMeasure α)
m✝ m : OuterMeasure α
s : ℕ → Set α
h_mono : ∀ (n : ℕ), s n ⊆ s (n + 1)
h0 : (∑' (k : ℕ), ↑m (s (k + 1) \ s k)) ≠ ⊤
inst✝ : (i : ℕ) → DecidablePred fun x => x ∈ s i
n : ℕ
h' : Monotone s
⊢ (⋃ (n : ℕ), s n) \ s n ⊆ ⋃ (i : ℕ), s (i + n + 1) \ s (i + n)
α : Type u_1
β : Type ?u.15791
R : Type ?u.15794
R' : Type ?u.15797
ms : Set (OuterMeasure α)
m✝ m : OuterMeasure α
s : ℕ → Set α
h_mono : ∀ (n : ℕ), s n ⊆ s (n + 1)
h0 : (∑' (k : ℕ), ↑m (s (k + 1) \ s k)) ≠ ⊤
inst✝ : (i : ℕ) → DecidablePred fun x => x ∈ s i
n : ℕ
⊢ (⋃ (n : ℕ), s n) \ s n ⊆ ⋃ (i : ℕ), s (i + n + 1) \ s (i + n)
have h' : Monotone s := @monotone_nat_of_le_succ (Set α) _ _ h_mono
α : Type u_1
β : Type ?u.15791
R : Type ?u.15794
R' : Type ?u.15797
ms : Set (OuterMeasure α)
m✝ m : OuterMeasure α
s : ℕ → Set α
h_mono : ∀ (n : ℕ), s n ⊆ s (n + 1)
h0 : (∑' (k : ℕ), ↑m (s (k + 1) \ s k)) ≠ ⊤
inst✝ : (i : ℕ) → DecidablePred fun x => x ∈ s i
n : ℕ
h' : Monotone s
⊢ ∀ (i : ℕ), s i ⊆ s n ∪ ⋃ (i : ℕ), s (i + n + 1) \ s (i + n)
α : Type u_1
β : Type ?u.15791
R : Type ?u.15794
R' : Type ?u.15797
ms : Set (OuterMeasure α)
m✝ m : OuterMeasure α
s : ℕ → Set α
h_mono : ∀ (n : ℕ), s n ⊆ s (n + 1)
h0 : (∑' (k : ℕ), ↑m (s (k + 1) \ s k)) ≠ ⊤
inst✝ : (i : ℕ) → DecidablePred fun x => x ∈ s i
n : ℕ
h' : Monotone s
⊢ (⋃ (n : ℕ), s n) \ s n ⊆ ⋃ (i : ℕ), s (i + n + 1) \ s (i + n)
simp only [diff_subset_iff, iUnion_subset_iff]
α : Type u_1
β : Type ?u.15791
R : Type ?u.15794
R' : Type ?u.15797
ms : Set (OuterMeasure α)
m✝ m : OuterMeasure α
s : ℕ → Set α
h_mono : ∀ (n : ℕ), s n ⊆ s (n + 1)
h0 : (∑' (k : ℕ), ↑m (s (k + 1) \ s k)) ≠ ⊤
inst✝ : (i : ℕ) → DecidablePred fun x => x ∈ s i
n : ℕ
h' : Monotone s
i : ℕ
x : α
hx : x ∈ s i
⊢ x ∈ s n ∪ ⋃ (i : ℕ), s (i + n + 1) \ s (i + n)
α : Type u_1
β : Type ?u.15791
R : Type ?u.15794
R' : Type ?u.15797
ms : Set (OuterMeasure α)
m✝ m : OuterMeasure α
s : ℕ → Set α
h_mono : ∀ (n : ℕ), s n ⊆ s (n + 1)
h0 : (∑' (k : ℕ), ↑m (s (k + 1) \ s k)) ≠ ⊤
inst✝ : (i : ℕ) → DecidablePred fun x => x ∈ s i
n : ℕ
h' : Monotone s
⊢ ∀ (i : ℕ), s i ⊆ s n ∪ ⋃ (i : ℕ), s (i + n + 1) \ s (i + n)
intro i x hx
α : Type u_1
β : Type ?u.15791
R : Type ?u.15794
R' : Type ?u.15797
ms : Set (OuterMeasure α)
m✝ m : OuterMeasure α
s : ℕ → Set α
h_mono : ∀ (n : ℕ), s n ⊆ s (n + 1)
h0 : (∑' (k : ℕ), ↑m (s (k + 1) \ s k)) ≠ ⊤
inst✝ : (i : ℕ) → DecidablePred fun x => x ∈ s i
n : ℕ
h' : Monotone s
i : ℕ
x : α
hx : x ∈ s i
this : ∃ i, x ∈ s i
⊢ x ∈ s n ∪ ⋃ (i : ℕ), s (i + n + 1) \ s (i + n)
α : Type u_1
β : Type ?u.15791
R : Type ?u.15794
R' : Type ?u.15797
ms : Set (OuterMeasure α)
m✝ m : OuterMeasure α
s : ℕ → Set α
h_mono : ∀ (n : ℕ), s n ⊆ s (n + 1)
h0 : (∑' (k : ℕ), ↑m (s (k + 1) \ s k)) ≠ ⊤
inst✝ : (i : ℕ) → DecidablePred fun x => x ∈ s i
n : ℕ
h' : Monotone s
i : ℕ
x : α
hx : x ∈ s i
⊢ x ∈ s n ∪ ⋃ (i : ℕ), s (i + n + 1) \ s (i + n)
have : ∃i, x ∈ s i := by exists i
case mk.intro
α : Type u_1
β : Type ?u.15791
R : Type ?u.15794
R' : Type ?u.15797
ms : Set (OuterMeasure α)
m✝ m : OuterMeasure α
s : ℕ → Set α
h_mono : ∀ (n : ℕ), s n ⊆ s (n + 1)
h0 : (∑' (k : ℕ), ↑m (s (k + 1) \ s k)) ≠ ⊤
inst✝ : (i : ℕ) → DecidablePred fun x => x ∈ s i
n : ℕ
h' : Monotone s
i : ℕ
x : α
hx : x ∈ s i
this : ∃ i, x ∈ s i
j : ℕ
hj : x ∈ s j
hlt : ∀ (m : ℕ), m < j → ¬x ∈ s m
⊢ x ∈ s n ∪ ⋃ (i : ℕ), s (i + n + 1) \ s (i + n)
α : Type u_1
β : Type ?u.15791
R : Type ?u.15794
R' : Type ?u.15797
ms : Set (OuterMeasure α)
m✝ m : OuterMeasure α
s : ℕ → Set α
h_mono : ∀ (n : ℕ), s n ⊆ s (n + 1)
h0 : (∑' (k : ℕ), ↑m (s (k + 1) \ s k)) ≠ ⊤
inst✝ : (i : ℕ) → DecidablePred fun x => x ∈ s i
n : ℕ
h' : Monotone s
i : ℕ
x : α
hx : x ∈ s i
this : ∃ i, x ∈ s i
⊢ x ∈ s n ∪ ⋃ (i : ℕ), s (i + n + 1) \ s (i + n)
rcases Nat.findX this with ⟨j, hj, hlt⟩
case mk.intro
α : Type u_1
β : Type ?u.15791
R : Type ?u.15794
R' : Type ?u.15797
ms : Set (OuterMeasure α)
m✝ m : OuterMeasure α
s : ℕ → Set α
h_mono : ∀ (n : ℕ), s n ⊆ s (n + 1)
h0 : (∑' (k : ℕ), ↑m (s (k + 1) \ s k)) ≠ ⊤
inst✝ : (i : ℕ) → DecidablePred fun x => x ∈ s i
n : ℕ
h' : Monotone s
x : α
this : ∃ i, x ∈ s i
j : ℕ
hj : x ∈ s j
hlt : ∀ (m : ℕ), m < j → ¬x ∈ s m
⊢ x ∈ s n ∪ ⋃ (i : ℕ), s (i + n + 1) \ s (i + n)
case mk.intro
α : Type u_1
β : Type ?u.15791
R : Type ?u.15794
R' : Type ?u.15797
ms : Set (OuterMeasure α)
m✝ m : OuterMeasure α
s : ℕ → Set α
h_mono : ∀ (n : ℕ), s n ⊆ s (n + 1)
h0 : (∑' (k : ℕ), ↑m (s (k + 1) \ s k)) ≠ ⊤
inst✝ : (i : ℕ) → DecidablePred fun x => x ∈ s i
n : ℕ
h' : Monotone s
i : ℕ
x : α
hx : x ∈ s i
this : ∃ i, x ∈ s i
j : ℕ
hj : x ∈ s j
hlt : ∀ (m : ℕ), m < j → ¬x ∈ s m
⊢ x ∈ s n ∪ ⋃ (i : ℕ), s (i + n + 1) \ s (i + n)
clear hx i
case mk.intro.inl
α : Type u_1
β : Type ?u.15791
R : Type ?u.15794
R' : Type ?u.15797
ms : Set (OuterMeasure α)
m✝ m : OuterMeasure α
s : ℕ → Set α
h_mono : ∀ (n : ℕ), s n ⊆ s (n + 1)
h0 : (∑' (k : ℕ), ↑m (s (k + 1) \ s k)) ≠ ⊤
inst✝ : (i : ℕ) → DecidablePred fun x => x ∈ s i
n : ℕ
h' : Monotone s
x : α
this : ∃ i, x ∈ s i
j : ℕ
hj : x ∈ s j
hlt : ∀ (m : ℕ), m < j → ¬x ∈ s m
hjn : j ≤ n
⊢ x ∈ s n ∪ ⋃ (i : ℕ), s (i + n + 1) \ s (i + n)

case mk.intro.inr
α : Type u_1
β : Type ?u.15791
R : Type ?u.15794
R' : Type ?u.15797
ms : Set (OuterMeasure α)
m✝ m : OuterMeasure α
s : ℕ → Set α
h_mono : ∀ (n : ℕ), s n ⊆ s (n + 1)
h0 : (∑' (k : ℕ), ↑m (s (k + 1) \ s k)) ≠ ⊤
inst✝ : (i : ℕ) → DecidablePred fun x => x ∈ s i
n : ℕ
h' : Monotone s
x : α
this : ∃ i, x ∈ s i
j : ℕ
hj : x ∈ s j
hlt : ∀ (m : ℕ), m < j → ¬x ∈ s m
hnj : n < j
⊢ x ∈ s n ∪ ⋃ (i : ℕ), s (i + n + 1) \ s (i + n)
case mk.intro
α : Type u_1
β : Type ?u.15791
R : Type ?u.15794
R' : Type ?u.15797
ms : Set (OuterMeasure α)
m✝ m : OuterMeasure α
s : ℕ → Set α
h_mono : ∀ (n : ℕ), s n ⊆ s (n + 1)
h0 : (∑' (k : ℕ), ↑m (s (k + 1) \ s k)) ≠ ⊤
inst✝ : (i : ℕ) → DecidablePred fun x => x ∈ s i
n : ℕ
h' : Monotone s
x : α
this : ∃ i, x ∈ s i
j : ℕ
hj : x ∈ s j
hlt : ∀ (m : ℕ), m < j → ¬x ∈ s m
⊢ x ∈ s n ∪ ⋃ (i : ℕ), s (i + n + 1) \ s (i + n)
cases' le_or_lt j n with hjn hnj
case mk.intro.inr
α : Type u_1
β : Type ?u.15791
R : Type ?u.15794
R' : Type ?u.15797
ms : Set (OuterMeasure α)
m✝ m : OuterMeasure α
s : ℕ → Set α
h_mono : ∀ (n : ℕ), s n ⊆ s (n + 1)
h0 : (∑' (k : ℕ), ↑m (s (k + 1) \ s k)) ≠ ⊤
inst✝ : (i : ℕ) → DecidablePred fun x => x ∈ s i
n : ℕ
h' : Monotone s
x : α
this✝ : ∃ i, x ∈ s i
j : ℕ
hj : x ∈ s j
hlt : ∀ (m : ℕ), m < j → ¬x ∈ s m
hnj : n < j
this : j - (n + 1) + n + 1 = j
⊢ x ∈ s n ∪ ⋃ (i : ℕ), s (i + n + 1) \ s (i + n)
case mk.intro.inr
α : Type u_1
β : Type ?u.15791
R : Type ?u.15794
R' : Type ?u.15797
ms : Set (OuterMeasure α)
m✝ m : OuterMeasure α
s : ℕ → Set α
h_mono : ∀ (n : ℕ), s n ⊆ s (n + 1)
h0 : (∑' (k : ℕ), ↑m (s (k + 1) \ s k)) ≠ ⊤
inst✝ : (i : ℕ) → DecidablePred fun x => x ∈ s i
n : ℕ
h' : Monotone s
x : α
this : ∃ i, x ∈ s i
j : ℕ
hj : x ∈ s j
hlt : ∀ (m : ℕ), m < j → ¬x ∈ s m
hnj : n < j
⊢ x ∈ s n ∪ ⋃ (i : ℕ), s (i + n + 1) \ s (i + n)
have : j - (n + 1) + n + 1 = j := by rw [add_assoc, tsub_add_cancel_of_le hnj.nat_succ_le]
case mk.intro.inr.refine'_1
α : Type u_1
β : Type ?u.15791
R : Type ?u.15794
R' : Type ?u.15797
ms : Set (OuterMeasure α)
m✝ m : OuterMeasure α
s : ℕ → Set α
h_mono : ∀ (n : ℕ), s n ⊆ s (n + 1)
h0 : (∑' (k : ℕ), ↑m (s (k + 1) \ s k)) ≠ ⊤
inst✝ : (i : ℕ) → DecidablePred fun x => x ∈ s i
n : ℕ
h' : Monotone s
x : α
this✝ : ∃ i, x ∈ s i
j : ℕ
hj : x ∈ s j
hlt : ∀ (m : ℕ), m < j → ¬x ∈ s m
hnj : n < j
this : j - (n + 1) + n + 1 = j
⊢ x ∈ s (j - (n + 1) + n + 1)

case mk.intro.inr.refine'_2
α : Type u_1
β : Type ?u.15791
R : Type ?u.15794
R' : Type ?u.15797
ms : Set (OuterMeasure α)
m✝ m : OuterMeasure α
s : ℕ → Set α
h_mono : ∀ (n : ℕ), s n ⊆ s (n + 1)
h0 : (∑' (k : ℕ), ↑m (s (k + 1) \ s k)) ≠ ⊤
inst✝ : (i : ℕ) → DecidablePred fun x => x ∈ s i
n : ℕ
h' : Monotone s
x : α
this✝ : ∃ i, x ∈ s i
j : ℕ
hj : x ∈ s j
hlt : ∀ (m : ℕ), m < j → ¬x ∈ s m
hnj : n < j
this : j - (n + 1) + n + 1 = j
⊢ j - (n + 1) + n < j
case mk.intro.inr
α : Type u_1
β : Type ?u.15791
R : Type ?u.15794
R' : Type ?u.15797
ms : Set (OuterMeasure α)
m✝ m : OuterMeasure α
s : ℕ → Set α
h_mono : ∀ (n : ℕ), s n ⊆ s (n + 1)
h0 : (∑' (k : ℕ), ↑m (s (k + 1) \ s k)) ≠ ⊤
inst✝ : (i : ℕ) → DecidablePred fun x => x ∈ s i
n : ℕ
h' : Monotone s
x : α
this✝ : ∃ i, x ∈ s i
j : ℕ
hj : x ∈ s j
hlt : ∀ (m : ℕ), m < j → ¬x ∈ s m
hnj : n < j
this : j - (n + 1) + n + 1 = j
⊢ x ∈ s n ∪ ⋃ (i : ℕ), s (i + n + 1) \ s (i + n)
refine' Or.inr (mem_iUnion.2 ⟨j - (n + 1), _, hlt _ _⟩)
no goals
α : Type u_1
β : Type ?u.15791
R : Type ?u.15794
R' : Type ?u.15797
ms : Set (OuterMeasure α)
m✝ m : OuterMeasure α
s : ℕ → Set α
h_mono : ∀ (n : ℕ), s n ⊆ s (n + 1)
h0 : (∑' (k : ℕ), ↑m (s (k + 1) \ s k)) ≠ ⊤
inst✝ : (i : ℕ) → DecidablePred fun x => x ∈ s i
n : ℕ
h' : Monotone s
i : ℕ
x : α
hx : x ∈ s i
⊢ ∃ i, x ∈ s i
exists i
no goals
case mk.intro.inl
α : Type u_1
β : Type ?u.15791
R : Type ?u.15794
R' : Type ?u.15797
ms : Set (OuterMeasure α)
m✝ m : OuterMeasure α
s : ℕ → Set α
h_mono : ∀ (n : ℕ), s n ⊆ s (n + 1)
h0 : (∑' (k : ℕ), ↑m (s (k + 1) \ s k)) ≠ ⊤
inst✝ : (i : ℕ) → DecidablePred fun x => x ∈ s i
n : ℕ
h' : Monotone s
x : α
this : ∃ i, x ∈ s i
j : ℕ
hj : x ∈ s j
hlt : ∀ (m : ℕ), m < j → ¬x ∈ s m
hjn : j ≤ n
⊢ x ∈ s n ∪ ⋃ (i : ℕ), s (i + n + 1) \ s (i + n)
exact Or.inl (h' hjn hj)
no goals
α : Type u_1
β : Type ?u.15791
R : Type ?u.15794
R' : Type ?u.15797
ms : Set (OuterMeasure α)
m✝ m : OuterMeasure α
s : ℕ → Set α
h_mono : ∀ (n : ℕ), s n ⊆ s (n + 1)
h0 : (∑' (k : ℕ), ↑m (s (k + 1) \ s k)) ≠ ⊤
inst✝ : (i : ℕ) → DecidablePred fun x => x ∈ s i
n : ℕ
h' : Monotone s
x : α
this : ∃ i, x ∈ s i
j : ℕ
hj : x ∈ s j
hlt : ∀ (m : ℕ), m < j → ¬x ∈ s m
hnj : n < j
⊢ j - (n + 1) + n + 1 = j
rw [add_assoc, tsub_add_cancel_of_le hnj.nat_succ_le]
no goals
case mk.intro.inr.refine'_1
α : Type u_1
β : Type ?u.15791
R : Type ?u.15794
R' : Type ?u.15797
ms : Set (OuterMeasure α)
m✝ m : OuterMeasure α
s : ℕ → Set α
h_mono : ∀ (n : ℕ), s n ⊆ s (n + 1)
h0 : (∑' (k : ℕ), ↑m (s (k + 1) \ s k)) ≠ ⊤
inst✝ : (i : ℕ) → DecidablePred fun x => x ∈ s i
n : ℕ
h' : Monotone s
x : α
this✝ : ∃ i, x ∈ s i
j : ℕ
hj : x ∈ s j
hlt : ∀ (m : ℕ), m < j → ¬x ∈ s m
hnj : n < j
this : j - (n + 1) + n + 1 = j
⊢ x ∈ s (j - (n + 1) + n + 1)
rwa [this]
no goals
case mk.intro.inr.refine'_2
α : Type u_1
β : Type ?u.15791
R : Type ?u.15794
R' : Type ?u.15797
ms : Set (OuterMeasure α)
m✝ m : OuterMeasure α
s : ℕ → Set α
h_mono : ∀ (n : ℕ), s n ⊆ s (n + 1)
h0 : (∑' (k : ℕ), ↑m (s (k + 1) \ s k)) ≠ ⊤
inst✝ : (i : ℕ) → DecidablePred fun x => x ∈ s i
n : ℕ
h' : Monotone s
x : α
this✝ : ∃ i, x ∈ s i
j : ℕ
hj : x ∈ s j
hlt : ∀ (m : ℕ), m < j → ¬x ∈ s m
hnj : n < j
this : j - (n + 1) + n + 1 = j
⊢ j - (n + 1) + n < j
rw [← Nat.succ_le_iff, Nat.succ_eq_add_one, this]