Theorems · Inductive type · measure theory

MeasurableEmbedding

{α : Type u_1} → {β : Type u_2} → [MeasurableSpace α] → [MeasurableSpace β] → (α → β) → Prop

A map f : α → β is called a measurable embedding if it is injective, measurable, and sends measurable sets to measurable sets. The latter assumption can be replaced with “f has measurable inverse g : Set.range f → α”, see MeasurableEmbedding.measurable_rangeSplitting, MeasurableEmbedding.of_measurable_inverse_range, and MeasurableEmbedding.of_measurable_inverse. One more interpretation: f is a measurable embedding if it defines a measurable equivalence to its range and the range is a measurable set. One implication is formalized as MeasurableEmbedding.equivRange; the other one follows from MeasurableEquiv.measurableEmbedding, MeasurableEmbedding.subtype_coe, and MeasurableEmbedding.comp.

Defined in

Mathlib.MeasureTheory.MeasurableSpace.Embedding

Cited by

170 results in Mathlib

Foundations

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

Assumes

MeasurableSpaceMeasurableSpace