Theorems · Inductive type · general topology

StandardBorelSpace

(α : Type u_1) → [MeasurableSpace α] → Prop

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

Cited by

304 results in Mathlib

Foundations

Depth 1 from the axioms, rests on 2 definitions · uses no axioms

Assumes

MeasurableSpace