English
For a measurable embedding f, there is a measurable equivalence between a set s and its image f''s.
Русский
При измеримом вложении f существует измеримая эквивалентность между множеством s и изображением f''s.
LaTeX
$$$ s \\simeq^m f''s $$$
Lean4
/-- A set is equivalent to its image under a function `f` as measurable spaces,
if `f` is a measurable embedding -/
noncomputable def equivImage (s : Set α) (hf : MeasurableEmbedding f) : s ≃ᵐ f '' s
where
toEquiv := Equiv.Set.image f s hf.injective
measurable_toFun := (hf.measurable.comp measurable_id.subtype_val).subtype_mk
measurable_invFun := by
rintro t ⟨u, hu, rfl⟩
simpa [preimage_preimage, Set.image_symm_preimage hf.injective] using
measurable_subtype_coe (hf.measurableSet_image' hu)