measurable_set_iff

Mathlib.MeasureTheory.MeasurableSpace.Constructions

URI: https://scilib.ai/kg/mathlib#measurable_set_iff

English

For g: β → Set α, Measurable g is equivalent to ∀ a, Measurable (x ↦ a ∈ g(x)).

Русский

Для g: β → Set α, измеримость g эквивалентна ∀ a, измеримости функции x ↦ (a ∈ g(x)).

LaTeX

$$$\mathrm{Measurable}(g) \iff \forall a, \mathrm{Measurable}(x \mapsto a \in g(x))$$$

Lean4

theorem measurable_set_iff : Measurable g ↔ ∀ a, Measurable fun x ↦ a ∈ g x :=
  measurable_pi_iff

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

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

Разделы

Аффилиация

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