measurableSet_mutuallySingularSet

Mathlib.Probability.Kernel.RadonNikodym

URI: https://scilib.ai/kg/mathlib#ProbabilityTheory.Kernel.measurableSet_mutuallySingularSet

← MathLib Explorer

English

The set κ.mutuallySingularSet η is a measurable subset of α×γ.

Русский

Множество κ.mutuallySingularSet η является измеримым подмножеством α×γ.

LaTeX

$$$\text{MeasurableSet}(\kappa.mutuallySingularSet(\eta))$$$

Lean4

theorem measurableSet_mutuallySingularSet (κ η : Kernel α γ) : MeasurableSet (mutuallySingularSet κ η) :=
  measurable_rnDerivAux κ (κ + η) measurableSet_Ici

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

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

Разделы

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

Аффилиация

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