α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
inst✝⁵ : MetricSpace β
μ : Measure α
inst✝⁴ : SemilatticeSup ι
inst✝³ : Nonempty ι
inst✝² : Countable ι
γ : Type ?u.46709
inst✝¹ : TopologicalSpace γ
f : ι → α → β
g : α → β
s : Set α
inst✝ : IsFiniteMeasure μ
hf : ∀ (n : ι), StronglyMeasurable (f n)
hg : StronglyMeasurable g
hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (g x))
ε : ℝ
hε : 0 < ε
t : Set α
w✝ : t ⊆ Set.univ
ht : MeasurableSet t
htendsto : ↑↑μ t ≤ ENNReal.ofReal ε ∧ TendstoUniformlyOn (fun n => f n) g atTop (Set.univ \ t)
⊢ ∃ t, MeasurableSet t ∧ ↑↑μ t ≤ ENNReal.ofReal ε ∧ TendstoUniformlyOn f g atTop (tᶜ)
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
inst✝⁵ : MetricSpace β
μ : Measure α
inst✝⁴ : SemilatticeSup ι
inst✝³ : Nonempty ι
inst✝² : Countable ι
γ : Type ?u.46709
inst✝¹ : TopologicalSpace γ
f : ι → α → β
g : α → β
s : Set α
inst✝ : IsFiniteMeasure μ
hf : ∀ (n : ι), StronglyMeasurable (f n)
hg : StronglyMeasurable g
hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (g x))
ε : ℝ
hε : 0 < ε
⊢ ∃ t, MeasurableSet t ∧ ↑↑μ t ≤ ENNReal.ofReal ε ∧ TendstoUniformlyOn f g atTop (tᶜ)
have ⟨t, _, ht, htendsto⟩ := tendstoUniformlyOn_of_ae_tendsto hf hg MeasurableSet.univ
  (measure_ne_top μ Set.univ) (by filter_upwards [hfg] with _ htendsto _ using htendsto) hε
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
inst✝⁵ : MetricSpace β
μ : Measure α
inst✝⁴ : SemilatticeSup ι
inst✝³ : Nonempty ι
inst✝² : Countable ι
γ : Type ?u.46709
inst✝¹ : TopologicalSpace γ
f : ι → α → β
g : α → β
s : Set α
inst✝ : IsFiniteMeasure μ
hf : ∀ (n : ι), StronglyMeasurable (f n)
hg : StronglyMeasurable g
hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (g x))
ε : ℝ
hε : 0 < ε
t : Set α
w✝ : t ⊆ Set.univ
ht : MeasurableSet t
htendsto : ↑↑μ t ≤ ENNReal.ofReal ε ∧ TendstoUniformlyOn (fun n => f n) g atTop (Set.univ \ t)
⊢ ↑↑μ t ≤ ENNReal.ofReal ε ∧ TendstoUniformlyOn f g atTop (tᶜ)
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
inst✝⁵ : MetricSpace β
μ : Measure α
inst✝⁴ : SemilatticeSup ι
inst✝³ : Nonempty ι
inst✝² : Countable ι
γ : Type ?u.46709
inst✝¹ : TopologicalSpace γ
f : ι → α → β
g : α → β
s : Set α
inst✝ : IsFiniteMeasure μ
hf : ∀ (n : ι), StronglyMeasurable (f n)
hg : StronglyMeasurable g
hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (g x))
ε : ℝ
hε : 0 < ε
t : Set α
w✝ : t ⊆ Set.univ
ht : MeasurableSet t
htendsto : ↑↑μ t ≤ ENNReal.ofReal ε ∧ TendstoUniformlyOn (fun n => f n) g atTop (Set.univ \ t)
⊢ ∃ t, MeasurableSet t ∧ ↑↑μ t ≤ ENNReal.ofReal ε ∧ TendstoUniformlyOn f g atTop (tᶜ)
refine' ⟨_, ht, _⟩
no goals
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
inst✝⁵ : MetricSpace β
μ : Measure α
inst✝⁴ : SemilatticeSup ι
inst✝³ : Nonempty ι
inst✝² : Countable ι
γ : Type ?u.46709
inst✝¹ : TopologicalSpace γ
f : ι → α → β
g : α → β
s : Set α
inst✝ : IsFiniteMeasure μ
hf : ∀ (n : ι), StronglyMeasurable (f n)
hg : StronglyMeasurable g
hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (g x))
ε : ℝ
hε : 0 < ε
t : Set α
w✝ : t ⊆ Set.univ
ht : MeasurableSet t
htendsto : ↑↑μ t ≤ ENNReal.ofReal ε ∧ TendstoUniformlyOn (fun n => f n) g atTop (Set.univ \ t)
⊢ ↑↑μ t ≤ ENNReal.ofReal ε ∧ TendstoUniformlyOn f g atTop (tᶜ)
rwa [Set.compl_eq_univ_diff]
no goals
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
inst✝⁵ : MetricSpace β
μ : Measure α
inst✝⁴ : SemilatticeSup ι
inst✝³ : Nonempty ι
inst✝² : Countable ι
γ : Type ?u.46709
inst✝¹ : TopologicalSpace γ
f : ι → α → β
g : α → β
s : Set α
inst✝ : IsFiniteMeasure μ
hf : ∀ (n : ι), StronglyMeasurable (f n)
hg : StronglyMeasurable g
hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (g x))
ε : ℝ
hε : 0 < ε
⊢ ∀ᵐ (x : α) ∂μ, x ∈ Set.univ → Tendsto (fun n => f n x) atTop (𝓝 (g x))
filter_upwards [hfg] with _ htendsto _ using htendsto