deterministic_map — Mathlib

English

Deterministic kernels are preserved under composition: deterministic f hf mapped by g equals deterministic (g ∘ f) with hg.comp hf.

Русский

Детерминированные ядра сохраняются при композиции: deterministic f hf.map g = deterministic (g ∘ f) (hg.comp hf).

LaTeX

$$$ (\operatorname{deterministic} f hf).map g = \operatorname{deterministic}(g \circ f)(hg \circ hf) $$$

Lean4

theorem deterministic_map {f : α → β} (hf : Measurable f) {g : β → γ} (hg : Measurable g) :
    (deterministic f hf).map g = deterministic (g ∘ f) (hg.comp hf) := by
  rw [← id_map, ← map_comp_right _ hf hg, id_map]

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