mathlib4 icon indicating copy to clipboard operation
mathlib4 copied to clipboard

Published 20 hours ago • verified publisher icon leanprover-community

feat: Ionescu-Tulcea theorem

Open EtienneC30 opened this issue 1 year ago • 0 comments

Work in progress.

We aim to prove Ionescu-Tulcea theorem, which implies the existence of a product measure for an arbitrary family of probability measures.

Open in Gitpod

EtienneC30 avatar May 24 '24 08:05 EtienneC30