const

Mathlib.MeasureTheory.Measure.NullMeasurable

URI: https://scilib.ai/kg/mathlib#MeasureTheory.NullMeasurableSet.const

English

Any constant predicate set is null measurable with respect to μ.

Русский

Любое константное множество множества: нулево измеримо относительно μ.

LaTeX

$$$\\text{NullMeasurableSet } \\{\\,x : \\alpha \\mid p\\,\\} μ$$$

Lean4

protected theorem const (p : Prop) : NullMeasurableSet {_a : α | p} μ :=
  MeasurableSet.const p

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

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

Разделы

Аффилиация

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