measurableSet_preimage — Mathlib

English

For a MeasurableEmbedding f and any s ⊆ β, MeasurableSet(f^{-1}[s]) is equivalent to MeasurableSet(s ∩ range(f)).

Русский

Для измеримого вложения f и любого множества s ⊆ β верно, что $f^{-1}[s]$ измеримо тогда и только тогда, когда $s ∩ \operatorname{range}(f)$ измеримо.

LaTeX

$$$\\text{MeasurableEmbedding}(f) \\Rightarrow \\forall s,\\ MeasurableSet(f^{-1}(s)) \\iff \\text{MeasurableSet}(s \\cap \\text{range}(f)).$$$

Lean4

theorem measurableSet_preimage (hf : MeasurableEmbedding f) {s : Set β} :
    MeasurableSet (f ⁻¹' s) ↔ MeasurableSet (s ∩ range f) := by
  rw [← image_preimage_eq_inter_range, hf.measurableSet_image]

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