Diff — Standard probability space

Revision #1589 → #2676 · back to history

modifiedJoint distribution of a sequence567bc3ad12af

Field	From #1589	To #2676
mathlib.decl	StandardBorelSpace.pi	StandardBorelSpace.pi_countable
provenance	ai	ai-moderated

modifiedProduct of countably many standard spaces7c842c275cb9

Field	From #1589	To #2676
mathlib.decl	StandardBorelSpace.pi	StandardBorelSpace.pi_countable
provenance	ai	ai-moderated