comap_map_comm — Mathlib

English

The operations comap and map commute: comap (map κ g) f hf = map (comap κ f hf) g.

Русский

Операции комап и квантификация совместимы: comap (map κ g) f hf = map (comap κ f hf) g.

LaTeX

$$$ \operatorname{comap}(\operatorname{map} \kappa g) f hf = \operatorname{map}(\operatorname{comap}(\kappa f hf) g)$$$

Lean4

theorem comap_map_comm (κ : Kernel β γ) {f : α → β} {g : γ → δ} (hf : Measurable f) (hg : Measurable g) :
    comap (map κ g) f hf = map (comap κ f hf) g := by
  ext x s _
  rw [comap_apply, map_apply _ hg, map_apply _ hg, comap_apply]

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