← Mathematical handbook

theorem Verification.copulaSample_ae_injective {Ω : Type u_1} [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] (C : ProbabilityTheory.Copula 2) (X : ℕ → Ω → Fin 2 → ↑unitInterval) (hX : ∀ (i : ℕ), Measurable (X i)) (hI : ProbabilityTheory.iIndepFun X μ) (hlaw : ∀ (i : ℕ), MeasureTheory.Measure.map (X i) μ = C.toMeasure) : ∀ᵐ (ω : Ω) ∂μ, ∀ (d : Fin 2), Function.Injective fun (i : ℕ) => X i ω d

Independent observations with uniform marginal laws have no coordinate ties, simultaneously over every pair in the infinite sample.