AtomlessMap.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Atomlessness of injective measurable pushforwards

This supports the standard-Borel-to-real reduction in the construction of measure-preserving maps.

theorem OAI.Problem356.nullSingletonClass_map_of_injective line 21

Source documentation

An injective measurable map preserves the property of having null singletons. No probability or finiteness hypothesis is needed.

theorem nullSingletonClass_map_of_injective (μ : Measure α)
    [NullSingletonClass μ] [MeasurableSingletonClass β]
    {f : α → β} (hf : Measurable f) (hinj : Function.Injective f) :
    NullSingletonClass (Measure.map f μ) := by
…

theorem OAI.Problem356.nullSingletonClass_map_embeddingReal line 36
Source documentation
The real-valued measurable embedding used for standard Borel spaces sends a singleton-null measure to a singleton-null real measure.
```
theorem nullSingletonClass_map_embeddingReal (μ : Measure α)
    [StandardBorelSpace α] [NullSingletonClass μ] :
    NullSingletonClass (Measure.map (embeddingReal α) μ) :=
…
```