aemeasurable_zero_measure

Mathlib.MeasureTheory.Measure.AEMeasurable

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

Lean4

@[simp, fun_prop, measurability]
theorem aemeasurable_zero_measure : AEMeasurable f (0 : Measure α) :=
  by
  nontriviality α; inhabit α
  exact ⟨fun _ => f default, measurable_const, rfl⟩

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

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

Разделы

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

Аффилиация

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