measurable_set_notMem

Mathlib.MeasureTheory.MeasurableSpace.Constructions

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

← MathLib Explorer

English

For a fixed a, the map s ↦ a ∉ s is measurable.

Русский

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

LaTeX

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

Lean4

@[aesop safe 100 apply (rule_sets := [Measurable])]
theorem measurable_set_notMem (a : α) : Measurable fun s : Set α ↦ a ∉ s :=
  (Measurable.of_discrete (f := Not)).comp <| measurable_set_mem a

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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