measurableSet_preimage_iff_preimage_val

English

Preimage of an analytic set under a continuous map is analytic.

Русский

Прообраз аналитического множества по непрерывному отображению аналитичен.

LaTeX

$$$\text{AnalyticSet}(s) \land \text{Continuous } f \Rightarrow \operatorname{AnalyticSet}(f^{-1}(s)).$$$

Lean4

/-- If `f : X → Z` is a Borel measurable map from a standard Borel space to a
countably separated measurable space then the preimage of a set `s` is measurable
if and only if the set is measurable in `Set.range f`. -/
theorem measurableSet_preimage_iff_preimage_val {f : X → Z} [CountablySeparated (range f)] (hf : Measurable f)
    {s : Set Z} : MeasurableSet (f ⁻¹' s) ↔ MeasurableSet ((↑) ⁻¹' s : Set (range f)) :=
  have hf' : Measurable (rangeFactorization f) := hf.subtype_mk
  hf'.measurableSet_preimage_iff_of_surjective (s := Subtype.val ⁻¹' s) rangeFactorization_surjective

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