← Mathematical handbook

theorem Verification.nelsen19_tendsto_zero {α : Type u_1} {l : Filter α} (θ : α → ℝ) (hθ : ∀ (a : α), 0 ≤ θ a) (ht : Filter.Tendsto θ l (nhds 0)) (u v : ↑unitInterval) : Filter.Tendsto (fun (a : α) => (nelsen19 (θ a) ⋯).cdf ![u, v]) l (nhds ((ProbabilityTheory.Copula.clayton 2 1 ⋯).cdf ![u, v]))