aemeasurable_dirac

Mathlib.MeasureTheory.Measure.Dirac

URI: https://scilib.ai/kg/mathlib#MeasureTheory.aemeasurable_dirac

← MathLib Explorer

English

The Dirac measure δ_a is finite (is a finite measure).

Русский

Мера Дирака δ_a конечна (является конечной мерой).

LaTeX

$$$ IsFiniteMeasure (dirac a) $$$

Lean4

@[fun_prop]
theorem aemeasurable_dirac [MeasurableSingletonClass α] {a : α} {f : α → β} : AEMeasurable f (Measure.dirac a) :=
  ⟨fun _ ↦ f a, measurable_const, ae_eq_dirac f⟩

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

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

Разделы

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

Аффилиация

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