le_dirac_apply

Mathlib.MeasureTheory.Measure.Dirac

URI: https://scilib.ai/kg/mathlib#MeasureTheory.Measure.le_dirac_apply

English

For any set s and point a, the Dirac measure of a on s takes only the values 0 or 1.

Русский

Мера Дирака в точке a на множество s принимает только значения 0 или 1.

LaTeX

$$$$ dirac(a, s) \in \{0,1\} $$$$

Lean4

theorem le_dirac_apply {a} : s.indicator 1 a ≤ dirac a s :=
  OuterMeasure.dirac_apply a s ▸ le_toMeasure_apply _ _ _

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

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

Разделы

Аффилиация

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