measurable_set_mem

Mathlib.MeasureTheory.MeasurableSpace.Constructions

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

English

For a fixed a ∈ α, the map s ↦ (a ∈ s) is measurable.

Русский

Для фиксированного a ∈ α отображение s ↦ (a ∈ s) измеримо.

LaTeX

$$$\mathrm{Measurable}(a \mapsto a \in s)$$$

Lean4

@[aesop safe 100 apply (rule_sets := [Measurable])]
theorem measurable_set_mem (a : α) : Measurable fun s : Set α ↦ a ∈ s :=
  measurable_pi_apply _

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

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

Разделы

Аффилиация

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