measurableSet_notMem

Mathlib.MeasureTheory.MeasurableSpace.Constructions

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

← MathLib Explorer

English

For a fixed a, the set {s : Set α | a ∉ s} is measurable.

Русский

Для фиксированного a множество {s : Set α | a ∉ s} измеримо.

LaTeX

$$$\mathrm{MeasurableSet}\{s : \mathrm{Set}(\alpha) \mid a \notin s\}$$$

Lean4

@[aesop safe 100 apply (rule_sets := [Measurable])]
theorem measurableSet_notMem (a : α) : MeasurableSet {s : Set α | a ∉ s} :=
  measurableSet_setOf.2 <| measurable_set_notMem _

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

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

Разделы

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

Аффилиация

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