case mp
Ω : Type u_2
inst✝² : Nonempty Ω
m0 : MeasurableSpace Ω
μ : FiniteMeasure Ω
inst✝¹ : TopologicalSpace Ω
inst✝ : OpensMeasurableSpace Ω
γ : Type u_1
F : Filter γ
μs : γ → FiniteMeasure Ω
nonzero : μ ≠ 0
⊢ Tendsto (fun i => normalize (μs i)) F (𝓝 (normalize μ)) ∧ Tendsto (fun i => mass (μs i)) F (𝓝 (mass μ)) →
    Tendsto μs F (𝓝 μ)

case mpr
Ω : Type u_2
inst✝² : Nonempty Ω
m0 : MeasurableSpace Ω
μ : FiniteMeasure Ω
inst✝¹ : TopologicalSpace Ω
inst✝ : OpensMeasurableSpace Ω
γ : Type u_1
F : Filter γ
μs : γ → FiniteMeasure Ω
nonzero : μ ≠ 0
⊢ Tendsto μs F (𝓝 μ) →
    Tendsto (fun i => normalize (μs i)) F (𝓝 (normalize μ)) ∧ Tendsto (fun i => mass (μs i)) F (𝓝 (mass μ))
Ω : Type u_2
inst✝² : Nonempty Ω
m0 : MeasurableSpace Ω
μ : FiniteMeasure Ω
inst✝¹ : TopologicalSpace Ω
inst✝ : OpensMeasurableSpace Ω
γ : Type u_1
F : Filter γ
μs : γ → FiniteMeasure Ω
nonzero : μ ≠ 0
⊢ Tendsto (fun i => normalize (μs i)) F (𝓝 (normalize μ)) ∧ Tendsto (fun i => mass (μs i)) F (𝓝 (mass μ)) ↔
    Tendsto μs F (𝓝 μ)
constructor
case mp.intro
Ω : Type u_2
inst✝² : Nonempty Ω
m0 : MeasurableSpace Ω
μ : FiniteMeasure Ω
inst✝¹ : TopologicalSpace Ω
inst✝ : OpensMeasurableSpace Ω
γ : Type u_1
F : Filter γ
μs : γ → FiniteMeasure Ω
nonzero : μ ≠ 0
normalized_lim : Tendsto (fun i => normalize (μs i)) F (𝓝 (normalize μ))
mass_lim : Tendsto (fun i => mass (μs i)) F (𝓝 (mass μ))
⊢ Tendsto μs F (𝓝 μ)
case mp
Ω : Type u_2
inst✝² : Nonempty Ω
m0 : MeasurableSpace Ω
μ : FiniteMeasure Ω
inst✝¹ : TopologicalSpace Ω
inst✝ : OpensMeasurableSpace Ω
γ : Type u_1
F : Filter γ
μs : γ → FiniteMeasure Ω
nonzero : μ ≠ 0
⊢ Tendsto (fun i => normalize (μs i)) F (𝓝 (normalize μ)) ∧ Tendsto (fun i => mass (μs i)) F (𝓝 (mass μ)) →
    Tendsto μs F (𝓝 μ)
rintro ⟨normalized_lim, mass_lim⟩
no goals
case mp.intro
Ω : Type u_2
inst✝² : Nonempty Ω
m0 : MeasurableSpace Ω
μ : FiniteMeasure Ω
inst✝¹ : TopologicalSpace Ω
inst✝ : OpensMeasurableSpace Ω
γ : Type u_1
F : Filter γ
μs : γ → FiniteMeasure Ω
nonzero : μ ≠ 0
normalized_lim : Tendsto (fun i => normalize (μs i)) F (𝓝 (normalize μ))
mass_lim : Tendsto (fun i => mass (μs i)) F (𝓝 (mass μ))
⊢ Tendsto μs F (𝓝 μ)
exact tendsto_of_tendsto_normalize_testAgainstNN_of_tendsto_mass normalized_lim mass_lim
case mpr
Ω : Type u_2
inst✝² : Nonempty Ω
m0 : MeasurableSpace Ω
μ : FiniteMeasure Ω
inst✝¹ : TopologicalSpace Ω
inst✝ : OpensMeasurableSpace Ω
γ : Type u_1
F : Filter γ
μs : γ → FiniteMeasure Ω
nonzero : μ ≠ 0
μs_lim : Tendsto μs F (𝓝 μ)
⊢ Tendsto (fun i => normalize (μs i)) F (𝓝 (normalize μ)) ∧ Tendsto (fun i => mass (μs i)) F (𝓝 (mass μ))
case mpr
Ω : Type u_2
inst✝² : Nonempty Ω
m0 : MeasurableSpace Ω
μ : FiniteMeasure Ω
inst✝¹ : TopologicalSpace Ω
inst✝ : OpensMeasurableSpace Ω
γ : Type u_1
F : Filter γ
μs : γ → FiniteMeasure Ω
nonzero : μ ≠ 0
⊢ Tendsto μs F (𝓝 μ) →
    Tendsto (fun i => normalize (μs i)) F (𝓝 (normalize μ)) ∧ Tendsto (fun i => mass (μs i)) F (𝓝 (mass μ))
intro μs_lim
no goals
case mpr
Ω : Type u_2
inst✝² : Nonempty Ω
m0 : MeasurableSpace Ω
μ : FiniteMeasure Ω
inst✝¹ : TopologicalSpace Ω
inst✝ : OpensMeasurableSpace Ω
γ : Type u_1
F : Filter γ
μs : γ → FiniteMeasure Ω
nonzero : μ ≠ 0
μs_lim : Tendsto μs F (𝓝 μ)
⊢ Tendsto (fun i => normalize (μs i)) F (𝓝 (normalize μ)) ∧ Tendsto (fun i => mass (μs i)) F (𝓝 (mass μ))
refine' ⟨tendsto_normalize_of_tendsto μs_lim nonzero, μs_lim.mass⟩