preimage

Mathlib.MeasureTheory.MeasurableSpace.Basic

URI: https://scilib.ai/kg/mathlib#MeasurableSet.preimage

English

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

Русский

Если f измерима и t измеримо, то прообраз f^{-1}(t) измерим.

LaTeX

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

Lean4

protected theorem preimage {t : Set β} (ht : MeasurableSet t) (hf : Measurable f) : MeasurableSet (f ⁻¹' t) :=
  hf ht

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru