comp_restrict — Mathlib

English

Restriction commutes with kernel composition: (η|s) ∘ κ = (η ∘ κ)|s.

Русский

Ограничение и композиция ядер взаимодействуют: (η|s) ∘ κ = (η ∘ κ)|s.

LaTeX

$$$(\\eta|_{s}) \\circ_k \\kappa = (\\eta \\circ_k \\kappa)|_{s}$$$

Lean4

theorem comp_restrict {s : Set γ} (hs : MeasurableSet s) : η.restrict hs ∘ₖ κ = (η ∘ₖ κ).restrict hs :=
  by
  ext a t ht
  simp_rw [comp_apply' _ _ _ ht, restrict_apply' _ _ _ ht, comp_apply' _ _ _ (ht.inter hs)]

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