← Mathematical handbook

theorem Verification.partition_coord_embed_self {n : ℕ} (P : ProbabilityTheory.Copula.IntervalPartition n) (i : Fin n) (u : ↑unitInterval) : P.coord i (partitionEmbed P i u) = u

theorem Verification.partition_coord_embed {n : ℕ} (P : ProbabilityTheory.Copula.IntervalPartition n) (i r : Fin n) (u : ↑unitInterval) : P.coord r (partitionEmbed P i u) = if r < i then 1 else if r = i then u else 0