map_apply'

Mathlib.Probability.Kernel.Composition.MapComap

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

← MathLib Explorer

English

For measurable f, and any measurable s, map κ f a s equals κ a (f^{-1}(s)).

Русский

Для измеримого f и любого измеримого s имеем map κ f a s = κ a (f^{-1}(s)).

LaTeX

$$$$\\text{map_apply'}(κ,f,a) (s) = κ a (f^{-1}(s)).$$$$

Lean4

theorem map_apply' (κ : Kernel α β) (hf : Measurable f) (a : α) {s : Set γ} (hs : MeasurableSet s) :
    map κ f a s = κ a (f ⁻¹' s) := by rw [map_apply _ hf, Measure.map_apply hf hs]

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

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

Разделы

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

Аффилиация

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