mem_measurableAtom_self

Mathlib.MeasureTheory.MeasurableSpace.Constructions

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

English

For every x in β, x ∈ measurableAtom(x).

Русский

Для каждого x в β выполняется x ∈ measurableAtom(x).

LaTeX

$$$$ x \in \operatorname{measurableAtom}(x) $$$$

Lean4

@[simp]
theorem mem_measurableAtom_self (x : β) : x ∈ measurableAtom x := by simp +contextual [measurableAtom]

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

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

Разделы

Аффилиация

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