Structures · Analysis

StandardBorelSpace

A standard Borel space is a measurable space arising as the Borel sets of some Polish topology. This is useful in situations where a space has no natural topology or the natural topology in a space is non-Polish. To endow a standard Borel space α with a compatible Polish topology, use letI := upgradeStandardBorel α. One can then use eq_borel_upgradeStandardBorel α to rewrite the MeasurableSpace α instance to borel α t, where t is the new topology.

Defined in

Mathlib.MeasureTheory.Constructions.Polish.Basic

Shape

One type argument · adds polish