theorem
Verification.copula_cdf_uniform_limit_of_pointwise
{ι : Type u_1}
{l : Filter ι}
{d : ℕ}
(C : ι → ProbabilityTheory.Copula d)
(F : (Fin d → ↑unitInterval) → ℝ)
(h : ∀ (u : Fin d → ↑unitInterval), Filter.Tendsto (fun (i : ι) => (C i).cdf u) l (nhds (F u)))
:
TendstoUniformly (fun (i : ι) => (C i).cdf) F l