Measurable embeddings out of countable spaces #
An injective measurable map out of a countable type into a type with measurable singletons is a measurable embedding: every subset of the domain is countable, hence so is its image, hence measurable.
Main results #
theorem
MeasurableEmbedding.of_injective_of_countable
{β : Type u_1}
{γ : Type u_2}
[MeasurableSpace β]
[MeasurableSpace γ]
[Countable β]
[MeasurableSingletonClass γ]
{f : β → γ}
(hf : Measurable f)
(hinj : Function.Injective f)
:
An injective measurable map out of a countable type into a type with measurable singletons is a measurable embedding.