theorem
Verification.copula_cdf_limit_of_moving_point
{ι : Type u_1}
{l : Filter ι}
(C : ι → ProbabilityTheory.Copula 2)
(v : ι → Fin 2 → ↑unitInterval)
(u : Fin 2 → ↑unitInterval)
{L : ℝ}
(hv : ∀ (j : Fin 2), Filter.Tendsto (fun (i : ι) => ↑(v i j)) l (nhds ↑(u j)))
(h : Filter.Tendsto (fun (i : ι) => (C i).cdf (v i)) l (nhds L))
:
Filter.Tendsto (fun (i : ι) => (C i).cdf u) l (nhds L)