Theorem Continuous.measurableEmbedding

Modification history

2025-06-19 19:44

Mathlib/MeasureTheory/Constructions/Polish/Basic.lean

feat: more API for monotone functions wrt topology (#26113)

Modified Continuous.measurableEmbedding View on Github →

2023-09-29 06:57

Mathlib/MeasureTheory/Constructions/Polish.lean

feat: add standard Borel space class (#7243) …

Modified Continuous.measurableEmbedding View on Github →

2023-05-21 16:29

Mathlib/MeasureTheory/Constructions/Polish.lean

feat: port MeasureTheory.Constructions.Polish (#4064)

Added Continuous.measurableEmbedding View on Github →