α : Type u_2
β : Type ?u.11198
R : Type ?u.11201
R' : Type ?u.11204
ms : Set (OuterMeasure α)
m✝ : OuterMeasure α
ι : Type u_1
m : OuterMeasure α
s : ι → Set α
l : Filter ι
inst✝ : NeBot l
S : Set α := ⋃ (n : ι), s n
h0 : Tendsto (fun k => ↑m (S \ s k)) l (𝓝 0)
⊢ ↑m S = ⨆ (n : ι), ↑m (s n)
α : Type u_2
β : Type ?u.11198
R : Type ?u.11201
R' : Type ?u.11204
ms : Set (OuterMeasure α)
m✝ : OuterMeasure α
ι : Type u_1
m : OuterMeasure α
s : ι → Set α
l : Filter ι
inst✝ : NeBot l
h0 : Tendsto (fun k => ↑m ((⋃ (n : ι), s n) \ s k)) l (𝓝 0)
⊢ ↑m (⋃ (n : ι), s n) = ⨆ (n : ι), ↑m (s n)
set S := ⋃ n, s n
α : Type u_2
β : Type ?u.11198
R : Type ?u.11201
R' : Type ?u.11204
ms : Set (OuterMeasure α)
m✝ : OuterMeasure α
ι : Type u_1
m : OuterMeasure α
s : ι → Set α
l : Filter ι
inst✝ : NeBot l
S : Set α := ⋃ (n : ι), s n
h0 : Tendsto (fun k => ↑m (S \ s k)) l (𝓝 0)
M : ℝ≥0∞ := ⨆ (n : ι), ↑m (s n)
⊢ ↑m S = M
α : Type u_2
β : Type ?u.11198
R : Type ?u.11201
R' : Type ?u.11204
ms : Set (OuterMeasure α)
m✝ : OuterMeasure α
ι : Type u_1
m : OuterMeasure α
s : ι → Set α
l : Filter ι
inst✝ : NeBot l
S : Set α := ⋃ (n : ι), s n
h0 : Tendsto (fun k => ↑m (S \ s k)) l (𝓝 0)
⊢ ↑m S = ⨆ (n : ι), ↑m (s n)
set M := ⨆ n, m (s n)
α : Type u_2
β : Type ?u.11198
R : Type ?u.11201
R' : Type ?u.11204
ms : Set (OuterMeasure α)
m✝ : OuterMeasure α
ι : Type u_1
m : OuterMeasure α
s : ι → Set α
l : Filter ι
inst✝ : NeBot l
S : Set α := ⋃ (n : ι), s n
h0 : Tendsto (fun k => ↑m (S \ s k)) l (𝓝 0)
M : ℝ≥0∞ := ⨆ (n : ι), ↑m (s n)
hsS : ∀ {k : ι}, s k ⊆ S
⊢ ↑m S = M
α : Type u_2
β : Type ?u.11198
R : Type ?u.11201
R' : Type ?u.11204
ms : Set (OuterMeasure α)
m✝ : OuterMeasure α
ι : Type u_1
m : OuterMeasure α
s : ι → Set α
l : Filter ι
inst✝ : NeBot l
S : Set α := ⋃ (n : ι), s n
h0 : Tendsto (fun k => ↑m (S \ s k)) l (𝓝 0)
M : ℝ≥0∞ := ⨆ (n : ι), ↑m (s n)
⊢ ↑m S = M
have hsS : ∀ {k}, s k ⊆ S := fun {k} => subset_iUnion _ _
α : Type u_2
β : Type ?u.11198
R : Type ?u.11201
R' : Type ?u.11204
ms : Set (OuterMeasure α)
m✝ : OuterMeasure α
ι : Type u_1
m : OuterMeasure α
s : ι → Set α
l : Filter ι
inst✝ : NeBot l
S : Set α := ⋃ (n : ι), s n
h0 : Tendsto (fun k => ↑m (S \ s k)) l (𝓝 0)
M : ℝ≥0∞ := ⨆ (n : ι), ↑m (s n)
hsS : ∀ {k : ι}, s k ⊆ S
⊢ ↑m S ≤ M
α : Type u_2
β : Type ?u.11198
R : Type ?u.11201
R' : Type ?u.11204
ms : Set (OuterMeasure α)
m✝ : OuterMeasure α
ι : Type u_1
m : OuterMeasure α
s : ι → Set α
l : Filter ι
inst✝ : NeBot l
S : Set α := ⋃ (n : ι), s n
h0 : Tendsto (fun k => ↑m (S \ s k)) l (𝓝 0)
M : ℝ≥0∞ := ⨆ (n : ι), ↑m (s n)
hsS : ∀ {k : ι}, s k ⊆ S
⊢ ↑m S = M
refine' le_antisymm _ (iSup_le fun n => m.mono hsS)
α : Type u_2
β : Type ?u.11198
R : Type ?u.11201
R' : Type ?u.11204
ms : Set (OuterMeasure α)
m✝ : OuterMeasure α
ι : Type u_1
m : OuterMeasure α
s : ι → Set α
l : Filter ι
inst✝ : NeBot l
S : Set α := ⋃ (n : ι), s n
h0 : Tendsto (fun k => ↑m (S \ s k)) l (𝓝 0)
M : ℝ≥0∞ := ⨆ (n : ι), ↑m (s n)
hsS : ∀ {k : ι}, s k ⊆ S
A : ∀ (k : ι), ↑m S ≤ M + ↑m (S \ s k)
⊢ ↑m S ≤ M
α : Type u_2
β : Type ?u.11198
R : Type ?u.11201
R' : Type ?u.11204
ms : Set (OuterMeasure α)
m✝ : OuterMeasure α
ι : Type u_1
m : OuterMeasure α
s : ι → Set α
l : Filter ι
inst✝ : NeBot l
S : Set α := ⋃ (n : ι), s n
h0 : Tendsto (fun k => ↑m (S \ s k)) l (𝓝 0)
M : ℝ≥0∞ := ⨆ (n : ι), ↑m (s n)
hsS : ∀ {k : ι}, s k ⊆ S
⊢ ↑m S ≤ M
have A : ∀ k, m S ≤ M + m (S \ s k) := fun k =>
  calc
    m S = m (s k ∪ S \ s k) := by rw [union_diff_self, union_eq_self_of_subset_left hsS]
    _ ≤ m (s k) + m (S \ s k) := (m.union _ _)
    _ ≤ M + m (S \ s k) := add_le_add_right (le_iSup (m.measureOf ∘ s) k) _
α : Type u_2
β : Type ?u.11198
R : Type ?u.11201
R' : Type ?u.11204
ms : Set (OuterMeasure α)
m✝ : OuterMeasure α
ι : Type u_1
m : OuterMeasure α
s : ι → Set α
l : Filter ι
inst✝ : NeBot l
S : Set α := ⋃ (n : ι), s n
h0 : Tendsto (fun k => ↑m (S \ s k)) l (𝓝 0)
M : ℝ≥0∞ := ⨆ (n : ι), ↑m (s n)
hsS : ∀ {k : ι}, s k ⊆ S
A : ∀ (k : ι), ↑m S ≤ M + ↑m (S \ s k)
B : Tendsto (fun k => M + ↑m (S \ s k)) l (𝓝 (M + 0))
⊢ ↑m S ≤ M
α : Type u_2
β : Type ?u.11198
R : Type ?u.11201
R' : Type ?u.11204
ms : Set (OuterMeasure α)
m✝ : OuterMeasure α
ι : Type u_1
m : OuterMeasure α
s : ι → Set α
l : Filter ι
inst✝ : NeBot l
S : Set α := ⋃ (n : ι), s n
h0 : Tendsto (fun k => ↑m (S \ s k)) l (𝓝 0)
M : ℝ≥0∞ := ⨆ (n : ι), ↑m (s n)
hsS : ∀ {k : ι}, s k ⊆ S
A : ∀ (k : ι), ↑m S ≤ M + ↑m (S \ s k)
⊢ ↑m S ≤ M
have B : Tendsto (fun k => M + m (S \ s k)) l (𝓝 (M + 0)) := tendsto_const_nhds.add h0
α : Type u_2
β : Type ?u.11198
R : Type ?u.11201
R' : Type ?u.11204
ms : Set (OuterMeasure α)
m✝ : OuterMeasure α
ι : Type u_1
m : OuterMeasure α
s : ι → Set α
l : Filter ι
inst✝ : NeBot l
S : Set α := ⋃ (n : ι), s n
h0 : Tendsto (fun k => ↑m (S \ s k)) l (𝓝 0)
M : ℝ≥0∞ := ⨆ (n : ι), ↑m (s n)
hsS : ∀ {k : ι}, s k ⊆ S
A : ∀ (k : ι), ↑m S ≤ M + ↑m (S \ s k)
B : Tendsto (fun k => M + ↑m (S \ s k)) l (𝓝 M)
⊢ ↑m S ≤ M
α : Type u_2
β : Type ?u.11198
R : Type ?u.11201
R' : Type ?u.11204
ms : Set (OuterMeasure α)
m✝ : OuterMeasure α
ι : Type u_1
m : OuterMeasure α
s : ι → Set α
l : Filter ι
inst✝ : NeBot l
S : Set α := ⋃ (n : ι), s n
h0 : Tendsto (fun k => ↑m (S \ s k)) l (𝓝 0)
M : ℝ≥0∞ := ⨆ (n : ι), ↑m (s n)
hsS : ∀ {k : ι}, s k ⊆ S
A : ∀ (k : ι), ↑m S ≤ M + ↑m (S \ s k)
B : Tendsto (fun k => M + ↑m (S \ s k)) l (𝓝 (M + 0))
⊢ ↑m S ≤ M
rw [add_zero] at B
no goals
α : Type u_2
β : Type ?u.11198
R : Type ?u.11201
R' : Type ?u.11204
ms : Set (OuterMeasure α)
m✝ : OuterMeasure α
ι : Type u_1
m : OuterMeasure α
s : ι → Set α
l : Filter ι
inst✝ : NeBot l
S : Set α := ⋃ (n : ι), s n
h0 : Tendsto (fun k => ↑m (S \ s k)) l (𝓝 0)
M : ℝ≥0∞ := ⨆ (n : ι), ↑m (s n)
hsS : ∀ {k : ι}, s k ⊆ S
A : ∀ (k : ι), ↑m S ≤ M + ↑m (S \ s k)
B : Tendsto (fun k => M + ↑m (S \ s k)) l (𝓝 M)
⊢ ↑m S ≤ M
exact ge_of_tendsto' B A
no goals
α : Type u_2
β : Type ?u.11198
R : Type ?u.11201
R' : Type ?u.11204
ms : Set (OuterMeasure α)
m✝ : OuterMeasure α
ι : Type u_1
m : OuterMeasure α
s : ι → Set α
l : Filter ι
inst✝ : NeBot l
S : Set α := ⋃ (n : ι), s n
h0 : Tendsto (fun k => ↑m (S \ s k)) l (𝓝 0)
M : ℝ≥0∞ := ⨆ (n : ι), ↑m (s n)
hsS : ∀ {k : ι}, s k ⊆ S
k : ι
⊢ ↑m S = ↑m (s k ∪ S \ s k)
rw [union_diff_self, union_eq_self_of_subset_left hsS]