restrict — Mathlib

English

For a kernel κ and a measurable set s, the restricted kernel κ|_s is defined by (κ|_s)(a) = κ(a)|_s.

Русский

Для ядра κ и измеримого множества s определено ограниченное ядро κ|_s таким образом: (κ|_s)(a) = κ(a)|_s.

LaTeX

$$$(\kappa|_s)(a) = \kappa(a)|_s$$$

Lean4

/-- Kernel given by the restriction of the measures in the image of a kernel to a set. -/
protected noncomputable def restrict (κ : Kernel α β) (hs : MeasurableSet s) : Kernel α β
    where
  toFun a := (κ a).restrict s
  measurable' := by
    refine Measure.measurable_of_measurable_coe _ fun t ht => ?_
    simp_rw [Measure.restrict_apply ht]
    exact Kernel.measurable_coe κ (ht.inter hs)

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