restrict_apply'

Mathlib.Probability.Kernel.Basic

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

← MathLib Explorer

English

For κ, hs measurable and a, the action on a set t is κ(a)(t ∩ s).

Русский

Для κ, hs измеримо и a, действие на множество t даёт κ(a)(t ∩ s).

LaTeX

$$$(\kappa|_s)(a)(t) = \kappa(a)(t \cap s)$$$

Lean4

theorem restrict_apply' (κ : Kernel α β) (hs : MeasurableSet s) (a : α) (ht : MeasurableSet t) :
    κ.restrict hs a t = (κ a) (t ∩ s) := by rw [restrict_apply κ hs a, Measure.restrict_apply ht]

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

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

Разделы

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

Аффилиация

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