Documentation

Copula.OrdinalSum.CountableSI

← Mathematical handbook
source
theorem ProbabilityTheory.Copula.countableOrdinalSumPi_diagonal_fixed (P : CountableIntervalPartition) (n : ℕ) :
(countableOrdinalSumPi P).diagonal (P.point n) = ↑(P.point n)

Every partition endpoint is a diagonal fixed point of the countable sum.

source
theorem ProbabilityTheory.Copula.countableOrdinalSumPi_isSI (P : CountableIntervalPartition) :
(countableOrdinalSumPi P).IsSI