measurableSet_preimage — Mathlib

English

If f is measurable and t is a measurable set, then the preimage f^{-1}(t) is measurable.

Русский

Если f измерима и t — измеримое множество, то его предварительная прообраз под f измерим.

LaTeX

$$$\\text{Measurable } f \\to \\text{MeasurableSet } t \\to \\text{MeasurableSet } (f^{-1} t)$$$

Lean4

@[measurability]
theorem measurableSet_preimage {t : Set β} (hf : Measurable f) (ht : MeasurableSet t) : MeasurableSet (f ⁻¹' t) :=
  hf ht

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