measurableSet_fiber

Mathlib.MeasureTheory.Function.SimpleFunc

URI: https://scilib.ai/kg/mathlib#MeasureTheory.SimpleFunc.measurableSet_fiber

English

For each x in β, the fiber {a ∈ α : f(a) = x} is a measurable set.

Русский

Для каждого x ∈ β множество-волокно {a ∈ α : f(a) = x} измеримо.

LaTeX

$$$\\text{MeasurableSet}(\\{a \\in \\alpha : f(a)=x\\})$$$

Lean4

theorem measurableSet_fiber (f : α →ₛ β) (x : β) : MeasurableSet (f ⁻¹' { x }) :=
  f.measurableSet_fiber' x

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

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

Разделы

Аффилиация

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