equivImage — Mathlib

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)

Похожие утверждения