measurableSet_mem

Mathlib.MeasureTheory.MeasurableSpace.Constructions

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

← MathLib Explorer

English

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

Русский

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

LaTeX

$$$\mathrm{MeasurableSet}\bigl\{s : \mathrm{Set}(\alpha) \mid a \in s\bigr\}$$$

Lean4

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

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

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

Разделы

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

Аффилиация

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