deterministic_comp_eq_map — Mathlib

English

If η is deterministic and κ is deterministic, then the composition is deterministic and equals the map induced by the composed function.

Русский

Если η и κ детерминированы, то их композиция детерминирована и равна отображению, вызываемому композицией функций.

LaTeX

$$$ (\text{deterministic } g) \circ_K (\text{deterministic } f) = \text{deterministic } (g \circ f)$$$

Lean4

theorem deterministic_comp_eq_map (hf : Measurable f) (κ : Kernel α β) : deterministic f hf ∘ₖ κ = map κ f :=
  by
  ext a s hs
  simp_rw [map_apply' _ hf _ hs, comp_apply' _ _ _ hs, deterministic_apply' hf _ hs,
    lintegral_indicator_const_comp hf hs, one_mul]

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