measurableSet_preimage — Mathlib

English

For a simple function f, the preimage of any set under its underlying map is measurable.

Русский

Для простой функции f предобраз любого множества по ее базовой карте измерим.

LaTeX

$$$\\mathrm{MeasurableSet}(f^{-1}(s))$ for any s$$

Lean4

@[measurability]
theorem measurableSet_preimage (f : α →ₛ β) (s) : MeasurableSet (f ⁻¹' s) :=
  measurableSet_cut (fun _ b => b ∈ s) f fun b => MeasurableSet.const (b ∈ s)

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