Theorem: TendstoUniformlyOn.integral_tendsto (Ray/Misc/Measure.lean)

State before:
E : Type
inst✝¹⁴ : NormedAddCommGroup E
inst✝¹³ : NormedSpace ℝ E
inst✝¹² : CompleteSpace E
inst✝¹¹ : SecondCountableTopology E
F : Type
inst✝¹⁰ : NormedAddCommGroup F
inst✝⁹ : NormedSpace ℝ F
inst✝⁸ : CompleteSpace F
X : Type
inst✝⁷ : MeasureSpace X
inst✝⁶ : MetricSpace X
inst✝⁵ : BorelSpace X
Y : Type
inst✝⁴ : MeasureSpace Y
inst✝³ : MetricSpace Y
inst✝² : BorelSpace Y
A : Type
inst✝¹ : TopologicalSpace A
f : ℕ → X → E
g : X → E
s : Set X
inst✝ : IsLocallyFiniteMeasure volume
u : TendstoUniformlyOn f g atTop s
fc : ∀ (n : ℕ), ContinuousOn (f n) s
sc : IsCompact s
⊢ Tendsto (fun n => ∫ (x : X) in s, f n x) atTop (𝓝 (∫ (x : X) in s, g x))
Tactic:
rcases u.uniformCauchySeqOn.bounded fc sc with ⟨b, _, bh⟩
State after:
case intro.intro
E : Type
inst✝¹⁴ : NormedAddCommGroup E
inst✝¹³ : NormedSpace ℝ E
inst✝¹² : CompleteSpace E
inst✝¹¹ : SecondCountableTopology E
F : Type
inst✝¹⁰ : NormedAddCommGroup F
inst✝⁹ : NormedSpace ℝ F
inst✝⁸ : CompleteSpace F
X : Type
inst✝⁷ : MeasureSpace X
inst✝⁶ : MetricSpace X
inst✝⁵ : BorelSpace X
Y : Type
inst✝⁴ : MeasureSpace Y
inst✝³ : MetricSpace Y
inst✝² : BorelSpace Y
A : Type
inst✝¹ : TopologicalSpace A
f : ℕ → X → E
g : X → E
s : Set X
inst✝ : IsLocallyFiniteMeasure volume
u : TendstoUniformlyOn f g atTop s
fc : ∀ (n : ℕ), ContinuousOn (f n) s
sc : IsCompact s
b : ℝ
left✝ : 0 ≤ b
bh : ∀ (n : ℕ), ∀ x ∈ s, ‖f n x‖ ≤ b
⊢ Tendsto (fun n => ∫ (x : X) in s, f n x) atTop (𝓝 (∫ (x : X) in s, g x))

State before:
case intro.intro
E : Type
inst✝¹⁴ : NormedAddCommGroup E
inst✝¹³ : NormedSpace ℝ E
inst✝¹² : CompleteSpace E
inst✝¹¹ : SecondCountableTopology E
F : Type
inst✝¹⁰ : NormedAddCommGroup F
inst✝⁹ : NormedSpace ℝ F
inst✝⁸ : CompleteSpace F
X : Type
inst✝⁷ : MeasureSpace X
inst✝⁶ : MetricSpace X
inst✝⁵ : BorelSpace X
Y : Type
inst✝⁴ : MeasureSpace Y
inst✝³ : MetricSpace Y
inst✝² : BorelSpace Y
A : Type
inst✝¹ : TopologicalSpace A
f : ℕ → X → E
g : X → E
s : Set X
inst✝ : IsLocallyFiniteMeasure volume
u : TendstoUniformlyOn f g atTop s
fc : ∀ (n : ℕ), ContinuousOn (f n) s
sc : IsCompact s
b : ℝ
left✝ : 0 ≤ b
bh : ∀ (n : ℕ), ∀ x ∈ s, ‖f n x‖ ≤ b
⊢ Tendsto (fun n => ∫ (x : X) in s, f n x) atTop (𝓝 (∫ (x : X) in s, g x))
Tactic:
apply tendsto_integral_of_dominated_convergence (F := f) (f := g) (fun _ ↦ b)
State after:
case intro.intro.F_measurable
E : Type
inst✝¹⁴ : NormedAddCommGroup E
inst✝¹³ : NormedSpace ℝ E
inst✝¹² : CompleteSpace E
inst✝¹¹ : SecondCountableTopology E
F : Type
inst✝¹⁰ : NormedAddCommGroup F
inst✝⁹ : NormedSpace ℝ F
inst✝⁸ : CompleteSpace F
X : Type
inst✝⁷ : MeasureSpace X
inst✝⁶ : MetricSpace X
inst✝⁵ : BorelSpace X
Y : Type
inst✝⁴ : MeasureSpace Y
inst✝³ : MetricSpace Y
inst✝² : BorelSpace Y
A : Type
inst✝¹ : TopologicalSpace A
f : ℕ → X → E
g : X → E
s : Set X
inst✝ : IsLocallyFiniteMeasure volume
u : TendstoUniformlyOn f g atTop s
fc : ∀ (n : ℕ), ContinuousOn (f n) s
sc : IsCompact s
b : ℝ
left✝ : 0 ≤ b
bh : ∀ (n : ℕ), ∀ x ∈ s, ‖f n x‖ ≤ b
⊢ ∀ (n : ℕ), AEStronglyMeasurable (f n) (volume.restrict s)

case intro.intro.bound_integrable
E : Type
inst✝¹⁴ : NormedAddCommGroup E
inst✝¹³ : NormedSpace ℝ E
inst✝¹² : CompleteSpace E
inst✝¹¹ : SecondCountableTopology E
F : Type
inst✝¹⁰ : NormedAddCommGroup F
inst✝⁹ : NormedSpace ℝ F
inst✝⁸ : CompleteSpace F
X : Type
inst✝⁷ : MeasureSpace X
inst✝⁶ : MetricSpace X
inst✝⁵ : BorelSpace X
Y : Type
inst✝⁴ : MeasureSpace Y
inst✝³ : MetricSpace Y
inst✝² : BorelSpace Y
A : Type
inst✝¹ : TopologicalSpace A
f : ℕ → X → E
g : X → E
s : Set X
inst✝ : IsLocallyFiniteMeasure volume
u : TendstoUniformlyOn f g atTop s
fc : ∀ (n : ℕ), ContinuousOn (f n) s
sc : IsCompact s
b : ℝ
left✝ : 0 ≤ b
bh : ∀ (n : ℕ), ∀ x ∈ s, ‖f n x‖ ≤ b
⊢ Integrable (fun x => b) (volume.restrict s)

case intro.intro.h_bound
E : Type
inst✝¹⁴ : NormedAddCommGroup E
inst✝¹³ : NormedSpace ℝ E
inst✝¹² : CompleteSpace E
inst✝¹¹ : SecondCountableTopology E
F : Type
inst✝¹⁰ : NormedAddCommGroup F
inst✝⁹ : NormedSpace ℝ F
inst✝⁸ : CompleteSpace F
X : Type
inst✝⁷ : MeasureSpace X
inst✝⁶ : MetricSpace X
inst✝⁵ : BorelSpace X
Y : Type
inst✝⁴ : MeasureSpace Y
inst✝³ : MetricSpace Y
inst✝² : BorelSpace Y
A : Type
inst✝¹ : TopologicalSpace A
f : ℕ → X → E
g : X → E
s : Set X
inst✝ : IsLocallyFiniteMeasure volume
u : TendstoUniformlyOn f g atTop s
fc : ∀ (n : ℕ), ContinuousOn (f n) s
sc : IsCompact s
b : ℝ
left✝ : 0 ≤ b
bh : ∀ (n : ℕ), ∀ x ∈ s, ‖f n x‖ ≤ b
⊢ ∀ (n : ℕ), ∀ᵐ (a : X) ∂volume.restrict s, ‖f n a‖ ≤ b

case intro.intro.h_lim
E : Type
inst✝¹⁴ : NormedAddCommGroup E
inst✝¹³ : NormedSpace ℝ E
inst✝¹² : CompleteSpace E
inst✝¹¹ : SecondCountableTopology E
F : Type
inst✝¹⁰ : NormedAddCommGroup F
inst✝⁹ : NormedSpace ℝ F
inst✝⁸ : CompleteSpace F
X : Type
inst✝⁷ : MeasureSpace X
inst✝⁶ : MetricSpace X
inst✝⁵ : BorelSpace X
Y : Type
inst✝⁴ : MeasureSpace Y
inst✝³ : MetricSpace Y
inst✝² : BorelSpace Y
A : Type
inst✝¹ : TopologicalSpace A
f : ℕ → X → E
g : X → E
s : Set X
inst✝ : IsLocallyFiniteMeasure volume
u : TendstoUniformlyOn f g atTop s
fc : ∀ (n : ℕ), ContinuousOn (f n) s
sc : IsCompact s
b : ℝ
left✝ : 0 ≤ b
bh : ∀ (n : ℕ), ∀ x ∈ s, ‖f n x‖ ≤ b
⊢ ∀ᵐ (a : X) ∂volume.restrict s, Tendsto (fun n => f n a) atTop (𝓝 (g a))

State before:
case intro.intro.F_measurable
E : Type
inst✝¹⁴ : NormedAddCommGroup E
inst✝¹³ : NormedSpace ℝ E
inst✝¹² : CompleteSpace E
inst✝¹¹ : SecondCountableTopology E
F : Type
inst✝¹⁰ : NormedAddCommGroup F
inst✝⁹ : NormedSpace ℝ F
inst✝⁸ : CompleteSpace F
X : Type
inst✝⁷ : MeasureSpace X
inst✝⁶ : MetricSpace X
inst✝⁵ : BorelSpace X
Y : Type
inst✝⁴ : MeasureSpace Y
inst✝³ : MetricSpace Y
inst✝² : BorelSpace Y
A : Type
inst✝¹ : TopologicalSpace A
f : ℕ → X → E
g : X → E
s : Set X
inst✝ : IsLocallyFiniteMeasure volume
u : TendstoUniformlyOn f g atTop s
fc : ∀ (n : ℕ), ContinuousOn (f n) s
sc : IsCompact s
b : ℝ
left✝ : 0 ≤ b
bh : ∀ (n : ℕ), ∀ x ∈ s, ‖f n x‖ ≤ b
⊢ ∀ (n : ℕ), AEStronglyMeasurable (f n) (volume.restrict s)
Tactic:
intro n
State after:
case intro.intro.F_measurable
E : Type
inst✝¹⁴ : NormedAddCommGroup E
inst✝¹³ : NormedSpace ℝ E
inst✝¹² : CompleteSpace E
inst✝¹¹ : SecondCountableTopology E
F : Type
inst✝¹⁰ : NormedAddCommGroup F
inst✝⁹ : NormedSpace ℝ F
inst✝⁸ : CompleteSpace F
X : Type
inst✝⁷ : MeasureSpace X
inst✝⁶ : MetricSpace X
inst✝⁵ : BorelSpace X
Y : Type
inst✝⁴ : MeasureSpace Y
inst✝³ : MetricSpace Y
inst✝² : BorelSpace Y
A : Type
inst✝¹ : TopologicalSpace A
f : ℕ → X → E
g : X → E
s : Set X
inst✝ : IsLocallyFiniteMeasure volume
u : TendstoUniformlyOn f g atTop s
fc : ∀ (n : ℕ), ContinuousOn (f n) s
sc : IsCompact s
b : ℝ
left✝ : 0 ≤ b
bh : ∀ (n : ℕ), ∀ x ∈ s, ‖f n x‖ ≤ b
n : ℕ
⊢ AEStronglyMeasurable (f n) (volume.restrict s)

State before:
case intro.intro.F_measurable
E : Type
inst✝¹⁴ : NormedAddCommGroup E
inst✝¹³ : NormedSpace ℝ E
inst✝¹² : CompleteSpace E
inst✝¹¹ : SecondCountableTopology E
F : Type
inst✝¹⁰ : NormedAddCommGroup F
inst✝⁹ : NormedSpace ℝ F
inst✝⁸ : CompleteSpace F
X : Type
inst✝⁷ : MeasureSpace X
inst✝⁶ : MetricSpace X
inst✝⁵ : BorelSpace X
Y : Type
inst✝⁴ : MeasureSpace Y
inst✝³ : MetricSpace Y
inst✝² : BorelSpace Y
A : Type
inst✝¹ : TopologicalSpace A
f : ℕ → X → E
g : X → E
s : Set X
inst✝ : IsLocallyFiniteMeasure volume
u : TendstoUniformlyOn f g atTop s
fc : ∀ (n : ℕ), ContinuousOn (f n) s
sc : IsCompact s
b : ℝ
left✝ : 0 ≤ b
bh : ∀ (n : ℕ), ∀ x ∈ s, ‖f n x‖ ≤ b
n : ℕ
⊢ AEStronglyMeasurable (f n) (volume.restrict s)
Tactic:
exact (fc n).aestronglyMeasurable sc.measurableSet
State after:
no goals

State before:
case intro.intro.bound_integrable
E : Type
inst✝¹⁴ : NormedAddCommGroup E
inst✝¹³ : NormedSpace ℝ E
inst✝¹² : CompleteSpace E
inst✝¹¹ : SecondCountableTopology E
F : Type
inst✝¹⁰ : NormedAddCommGroup F
inst✝⁹ : NormedSpace ℝ F
inst✝⁸ : CompleteSpace F
X : Type
inst✝⁷ : MeasureSpace X
inst✝⁶ : MetricSpace X
inst✝⁵ : BorelSpace X
Y : Type
inst✝⁴ : MeasureSpace Y
inst✝³ : MetricSpace Y
inst✝² : BorelSpace Y
A : Type
inst✝¹ : TopologicalSpace A
f : ℕ → X → E
g : X → E
s : Set X
inst✝ : IsLocallyFiniteMeasure volume
u : TendstoUniformlyOn f g atTop s
fc : ∀ (n : ℕ), ContinuousOn (f n) s
sc : IsCompact s
b : ℝ
left✝ : 0 ≤ b
bh : ∀ (n : ℕ), ∀ x ∈ s, ‖f n x‖ ≤ b
⊢ Integrable (fun x => b) (volume.restrict s)
Tactic:
exact continuousOn_const.integrableOn_compact sc
State after:
no goals

State before:
case intro.intro.h_bound
E : Type
inst✝¹⁴ : NormedAddCommGroup E
inst✝¹³ : NormedSpace ℝ E
inst✝¹² : CompleteSpace E
inst✝¹¹ : SecondCountableTopology E
F : Type
inst✝¹⁰ : NormedAddCommGroup F
inst✝⁹ : NormedSpace ℝ F
inst✝⁸ : CompleteSpace F
X : Type
inst✝⁷ : MeasureSpace X
inst✝⁶ : MetricSpace X
inst✝⁵ : BorelSpace X
Y : Type
inst✝⁴ : MeasureSpace Y
inst✝³ : MetricSpace Y
inst✝² : BorelSpace Y
A : Type
inst✝¹ : TopologicalSpace A
f : ℕ → X → E
g : X → E
s : Set X
inst✝ : IsLocallyFiniteMeasure volume
u : TendstoUniformlyOn f g atTop s
fc : ∀ (n : ℕ), ContinuousOn (f n) s
sc : IsCompact s
b : ℝ
left✝ : 0 ≤ b
bh : ∀ (n : ℕ), ∀ x ∈ s, ‖f n x‖ ≤ b
⊢ ∀ (n : ℕ), ∀ᵐ (a : X) ∂volume.restrict s, ‖f n a‖ ≤ b
Tactic:
intro n
State after:
case intro.intro.h_bound
E : Type
inst✝¹⁴ : NormedAddCommGroup E
inst✝¹³ : NormedSpace ℝ E
inst✝¹² : CompleteSpace E
inst✝¹¹ : SecondCountableTopology E
F : Type
inst✝¹⁰ : NormedAddCommGroup F
inst✝⁹ : NormedSpace ℝ F
inst✝⁸ : CompleteSpace F
X : Type
inst✝⁷ : MeasureSpace X
inst✝⁶ : MetricSpace X
inst✝⁵ : BorelSpace X
Y : Type
inst✝⁴ : MeasureSpace Y
inst✝³ : MetricSpace Y
inst✝² : BorelSpace Y
A : Type
inst✝¹ : TopologicalSpace A
f : ℕ → X → E
g : X → E
s : Set X
inst✝ : IsLocallyFiniteMeasure volume
u : TendstoUniformlyOn f g atTop s
fc : ∀ (n : ℕ), ContinuousOn (f n) s
sc : IsCompact s
b : ℝ
left✝ : 0 ≤ b
bh : ∀ (n : ℕ), ∀ x ∈ s, ‖f n x‖ ≤ b
n : ℕ
⊢ ∀ᵐ (a : X) ∂volume.restrict s, ‖f n a‖ ≤ b

State before:
case intro.intro.h_bound
E : Type
inst✝¹⁴ : NormedAddCommGroup E
inst✝¹³ : NormedSpace ℝ E
inst✝¹² : CompleteSpace E
inst✝¹¹ : SecondCountableTopology E
F : Type
inst✝¹⁰ : NormedAddCommGroup F
inst✝⁹ : NormedSpace ℝ F
inst✝⁸ : CompleteSpace F
X : Type
inst✝⁷ : MeasureSpace X
inst✝⁶ : MetricSpace X
inst✝⁵ : BorelSpace X
Y : Type
inst✝⁴ : MeasureSpace Y
inst✝³ : MetricSpace Y
inst✝² : BorelSpace Y
A : Type
inst✝¹ : TopologicalSpace A
f : ℕ → X → E
g : X → E
s : Set X
inst✝ : IsLocallyFiniteMeasure volume
u : TendstoUniformlyOn f g atTop s
fc : ∀ (n : ℕ), ContinuousOn (f n) s
sc : IsCompact s
b : ℝ
left✝ : 0 ≤ b
bh : ∀ (n : ℕ), ∀ x ∈ s, ‖f n x‖ ≤ b
n : ℕ
⊢ ∀ᵐ (a : X) ∂volume.restrict s, ‖f n a‖ ≤ b
Tactic:
specialize bh n
State after:
case intro.intro.h_bound
E : Type
inst✝¹⁴ : NormedAddCommGroup E
inst✝¹³ : NormedSpace ℝ E
inst✝¹² : CompleteSpace E
inst✝¹¹ : SecondCountableTopology E
F : Type
inst✝¹⁰ : NormedAddCommGroup F
inst✝⁹ : NormedSpace ℝ F
inst✝⁸ : CompleteSpace F
X : Type
inst✝⁷ : MeasureSpace X
inst✝⁶ : MetricSpace X
inst✝⁵ : BorelSpace X
Y : Type
inst✝⁴ : MeasureSpace Y
inst✝³ : MetricSpace Y
inst✝² : BorelSpace Y
A : Type
inst✝¹ : TopologicalSpace A
f : ℕ → X → E
g : X → E
s : Set X
inst✝ : IsLocallyFiniteMeasure volume
u : TendstoUniformlyOn f g atTop s
fc : ∀ (n : ℕ), ContinuousOn (f n) s
sc : IsCompact s
b : ℝ
left✝ : 0 ≤ b
n : ℕ
bh : ∀ x ∈ s, ‖f n x‖ ≤ b
⊢ ∀ᵐ (a : X) ∂volume.restrict s, ‖f n a‖ ≤ b

State before:
case intro.intro.h_bound
E : Type
inst✝¹⁴ : NormedAddCommGroup E
inst✝¹³ : NormedSpace ℝ E
inst✝¹² : CompleteSpace E
inst✝¹¹ : SecondCountableTopology E
F : Type
inst✝¹⁰ : NormedAddCommGroup F
inst✝⁹ : NormedSpace ℝ F
inst✝⁸ : CompleteSpace F
X : Type
inst✝⁷ : MeasureSpace X
inst✝⁶ : MetricSpace X
inst✝⁵ : BorelSpace X
Y : Type
inst✝⁴ : MeasureSpace Y
inst✝³ : MetricSpace Y
inst✝² : BorelSpace Y
A : Type
inst✝¹ : TopologicalSpace A
f : ℕ → X → E
g : X → E
s : Set X
inst✝ : IsLocallyFiniteMeasure volume
u : TendstoUniformlyOn f g atTop s
fc : ∀ (n : ℕ), ContinuousOn (f n) s
sc : IsCompact s
b : ℝ
left✝ : 0 ≤ b
n : ℕ
bh : ∀ x ∈ s, ‖f n x‖ ≤ b
⊢ ∀ᵐ (a : X) ∂volume.restrict s, ‖f n a‖ ≤ b
Tactic:
rw [ae_restrict_iff' sc.measurableSet]
State after:
case intro.intro.h_bound
E : Type
inst✝¹⁴ : NormedAddCommGroup E
inst✝¹³ : NormedSpace ℝ E
inst✝¹² : CompleteSpace E
inst✝¹¹ : SecondCountableTopology E
F : Type
inst✝¹⁰ : NormedAddCommGroup F
inst✝⁹ : NormedSpace ℝ F
inst✝⁸ : CompleteSpace F
X : Type
inst✝⁷ : MeasureSpace X
inst✝⁶ : MetricSpace X
inst✝⁵ : BorelSpace X
Y : Type
inst✝⁴ : MeasureSpace Y
inst✝³ : MetricSpace Y
inst✝² : BorelSpace Y
A : Type
inst✝¹ : TopologicalSpace A
f : ℕ → X → E
g : X → E
s : Set X
inst✝ : IsLocallyFiniteMeasure volume
u : TendstoUniformlyOn f g atTop s
fc : ∀ (n : ℕ), ContinuousOn (f n) s
sc : IsCompact s
b : ℝ
left✝ : 0 ≤ b
n : ℕ
bh : ∀ x ∈ s, ‖f n x‖ ≤ b
⊢ ∀ᵐ (x : X), x ∈ s → ‖f n x‖ ≤ b

State before:
case intro.intro.h_bound
E : Type
inst✝¹⁴ : NormedAddCommGroup E
inst✝¹³ : NormedSpace ℝ E
inst✝¹² : CompleteSpace E
inst✝¹¹ : SecondCountableTopology E
F : Type
inst✝¹⁰ : NormedAddCommGroup F
inst✝⁹ : NormedSpace ℝ F
inst✝⁸ : CompleteSpace F
X : Type
inst✝⁷ : MeasureSpace X
inst✝⁶ : MetricSpace X
inst✝⁵ : BorelSpace X
Y : Type
inst✝⁴ : MeasureSpace Y
inst✝³ : MetricSpace Y
inst✝² : BorelSpace Y
A : Type
inst✝¹ : TopologicalSpace A
f : ℕ → X → E
g : X → E
s : Set X
inst✝ : IsLocallyFiniteMeasure volume
u : TendstoUniformlyOn f g atTop s
fc : ∀ (n : ℕ), ContinuousOn (f n) s
sc : IsCompact s
b : ℝ
left✝ : 0 ≤ b
n : ℕ
bh : ∀ x ∈ s, ‖f n x‖ ≤ b
⊢ ∀ᵐ (x : X), x ∈ s → ‖f n x‖ ≤ b
Tactic:
exact ae_of_all _ bh
State after:
no goals

State before:
case intro.intro.h_lim
E : Type
inst✝¹⁴ : NormedAddCommGroup E
inst✝¹³ : NormedSpace ℝ E
inst✝¹² : CompleteSpace E
inst✝¹¹ : SecondCountableTopology E
F : Type
inst✝¹⁰ : NormedAddCommGroup F
inst✝⁹ : NormedSpace ℝ F
inst✝⁸ : CompleteSpace F
X : Type
inst✝⁷ : MeasureSpace X
inst✝⁶ : MetricSpace X
inst✝⁵ : BorelSpace X
Y : Type
inst✝⁴ : MeasureSpace Y
inst✝³ : MetricSpace Y
inst✝² : BorelSpace Y
A : Type
inst✝¹ : TopologicalSpace A
f : ℕ → X → E
g : X → E
s : Set X
inst✝ : IsLocallyFiniteMeasure volume
u : TendstoUniformlyOn f g atTop s
fc : ∀ (n : ℕ), ContinuousOn (f n) s
sc : IsCompact s
b : ℝ
left✝ : 0 ≤ b
bh : ∀ (n : ℕ), ∀ x ∈ s, ‖f n x‖ ≤ b
⊢ ∀ᵐ (a : X) ∂volume.restrict s, Tendsto (fun n => f n a) atTop (𝓝 (g a))
Tactic:
rw [ae_restrict_iff' sc.measurableSet]
State after:
case intro.intro.h_lim
E : Type
inst✝¹⁴ : NormedAddCommGroup E
inst✝¹³ : NormedSpace ℝ E
inst✝¹² : CompleteSpace E
inst✝¹¹ : SecondCountableTopology E
F : Type
inst✝¹⁰ : NormedAddCommGroup F
inst✝⁹ : NormedSpace ℝ F
inst✝⁸ : CompleteSpace F
X : Type
inst✝⁷ : MeasureSpace X
inst✝⁶ : MetricSpace X
inst✝⁵ : BorelSpace X
Y : Type
inst✝⁴ : MeasureSpace Y
inst✝³ : MetricSpace Y
inst✝² : BorelSpace Y
A : Type
inst✝¹ : TopologicalSpace A
f : ℕ → X → E
g : X → E
s : Set X
inst✝ : IsLocallyFiniteMeasure volume
u : TendstoUniformlyOn f g atTop s
fc : ∀ (n : ℕ), ContinuousOn (f n) s
sc : IsCompact s
b : ℝ
left✝ : 0 ≤ b
bh : ∀ (n : ℕ), ∀ x ∈ s, ‖f n x‖ ≤ b
⊢ ∀ᵐ (x : X), x ∈ s → Tendsto (fun n => f n x) atTop (𝓝 (g x))

State before:
case intro.intro.h_lim
E : Type
inst✝¹⁴ : NormedAddCommGroup E
inst✝¹³ : NormedSpace ℝ E
inst✝¹² : CompleteSpace E
inst✝¹¹ : SecondCountableTopology E
F : Type
inst✝¹⁰ : NormedAddCommGroup F
inst✝⁹ : NormedSpace ℝ F
inst✝⁸ : CompleteSpace F
X : Type
inst✝⁷ : MeasureSpace X
inst✝⁶ : MetricSpace X
inst✝⁵ : BorelSpace X
Y : Type
inst✝⁴ : MeasureSpace Y
inst✝³ : MetricSpace Y
inst✝² : BorelSpace Y
A : Type
inst✝¹ : TopologicalSpace A
f : ℕ → X → E
g : X → E
s : Set X
inst✝ : IsLocallyFiniteMeasure volume
u : TendstoUniformlyOn f g atTop s
fc : ∀ (n : ℕ), ContinuousOn (f n) s
sc : IsCompact s
b : ℝ
left✝ : 0 ≤ b
bh : ∀ (n : ℕ), ∀ x ∈ s, ‖f n x‖ ≤ b
⊢ ∀ᵐ (x : X), x ∈ s → Tendsto (fun n => f n x) atTop (𝓝 (g x))
Tactic:
apply ae_of_all
State after:
case intro.intro.h_lim.a
E : Type
inst✝¹⁴ : NormedAddCommGroup E
inst✝¹³ : NormedSpace ℝ E
inst✝¹² : CompleteSpace E
inst✝¹¹ : SecondCountableTopology E
F : Type
inst✝¹⁰ : NormedAddCommGroup F
inst✝⁹ : NormedSpace ℝ F
inst✝⁸ : CompleteSpace F
X : Type
inst✝⁷ : MeasureSpace X
inst✝⁶ : MetricSpace X
inst✝⁵ : BorelSpace X
Y : Type
inst✝⁴ : MeasureSpace Y
inst✝³ : MetricSpace Y
inst✝² : BorelSpace Y
A : Type
inst✝¹ : TopologicalSpace A
f : ℕ → X → E
g : X → E
s : Set X
inst✝ : IsLocallyFiniteMeasure volume
u : TendstoUniformlyOn f g atTop s
fc : ∀ (n : ℕ), ContinuousOn (f n) s
sc : IsCompact s
b : ℝ
left✝ : 0 ≤ b
bh : ∀ (n : ℕ), ∀ x ∈ s, ‖f n x‖ ≤ b
⊢ ∀ a ∈ s, Tendsto (fun n => f n a) atTop (𝓝 (g a))

State before:
case intro.intro.h_lim.a
E : Type
inst✝¹⁴ : NormedAddCommGroup E
inst✝¹³ : NormedSpace ℝ E
inst✝¹² : CompleteSpace E
inst✝¹¹ : SecondCountableTopology E
F : Type
inst✝¹⁰ : NormedAddCommGroup F
inst✝⁹ : NormedSpace ℝ F
inst✝⁸ : CompleteSpace F
X : Type
inst✝⁷ : MeasureSpace X
inst✝⁶ : MetricSpace X
inst✝⁵ : BorelSpace X
Y : Type
inst✝⁴ : MeasureSpace Y
inst✝³ : MetricSpace Y
inst✝² : BorelSpace Y
A : Type
inst✝¹ : TopologicalSpace A
f : ℕ → X → E
g : X → E
s : Set X
inst✝ : IsLocallyFiniteMeasure volume
u : TendstoUniformlyOn f g atTop s
fc : ∀ (n : ℕ), ContinuousOn (f n) s
sc : IsCompact s
b : ℝ
left✝ : 0 ≤ b
bh : ∀ (n : ℕ), ∀ x ∈ s, ‖f n x‖ ≤ b
⊢ ∀ a ∈ s, Tendsto (fun n => f n a) atTop (𝓝 (g a))
Tactic:
intro x xs
State after:
case intro.intro.h_lim.a
E : Type
inst✝¹⁴ : NormedAddCommGroup E
inst✝¹³ : NormedSpace ℝ E
inst✝¹² : CompleteSpace E
inst✝¹¹ : SecondCountableTopology E
F : Type
inst✝¹⁰ : NormedAddCommGroup F
inst✝⁹ : NormedSpace ℝ F
inst✝⁸ : CompleteSpace F
X : Type
inst✝⁷ : MeasureSpace X
inst✝⁶ : MetricSpace X
inst✝⁵ : BorelSpace X
Y : Type
inst✝⁴ : MeasureSpace Y
inst✝³ : MetricSpace Y
inst✝² : BorelSpace Y
A : Type
inst✝¹ : TopologicalSpace A
f : ℕ → X → E
g : X → E
s : Set X
inst✝ : IsLocallyFiniteMeasure volume
u : TendstoUniformlyOn f g atTop s
fc : ∀ (n : ℕ), ContinuousOn (f n) s
sc : IsCompact s
b : ℝ
left✝ : 0 ≤ b
bh : ∀ (n : ℕ), ∀ x ∈ s, ‖f n x‖ ≤ b
x : X
xs : x ∈ s
⊢ Tendsto (fun n => f n x) atTop (𝓝 (g x))

State before:
case intro.intro.h_lim.a
E : Type
inst✝¹⁴ : NormedAddCommGroup E
inst✝¹³ : NormedSpace ℝ E
inst✝¹² : CompleteSpace E
inst✝¹¹ : SecondCountableTopology E
F : Type
inst✝¹⁰ : NormedAddCommGroup F
inst✝⁹ : NormedSpace ℝ F
inst✝⁸ : CompleteSpace F
X : Type
inst✝⁷ : MeasureSpace X
inst✝⁶ : MetricSpace X
inst✝⁵ : BorelSpace X
Y : Type
inst✝⁴ : MeasureSpace Y
inst✝³ : MetricSpace Y
inst✝² : BorelSpace Y
A : Type
inst✝¹ : TopologicalSpace A
f : ℕ → X → E
g : X → E
s : Set X
inst✝ : IsLocallyFiniteMeasure volume
u : TendstoUniformlyOn f g atTop s
fc : ∀ (n : ℕ), ContinuousOn (f n) s
sc : IsCompact s
b : ℝ
left✝ : 0 ≤ b
bh : ∀ (n : ℕ), ∀ x ∈ s, ‖f n x‖ ≤ b
x : X
xs : x ∈ s
⊢ Tendsto (fun n => f n x) atTop (𝓝 (g x))
Tactic:
exact u.tendsto_at xs
State after:
no goals