pi_comap — Mathlib

English

The Pi-construction commutes with comap: pi (i ↦ comap (f i) (l i)) = comap (Pi.map f) (pi l).

Русский

Прообразование по Pi-композиции совместимо: пи( i ↦ comap (f i) (l i) ) = comap (Pi.map f) (pi l).

LaTeX

$$$\\pi(\\lambda i.\\mathrm{comap}(f i)(l i)) = \\mathrm{comap}(\\Pi.map\,f)\,(\\pi\,l)$$$

Lean4

theorem pi_comap {β : ι → Type*} {f : ∀ i, α i → β i} {l : ∀ i, Filter (β i)} :
    pi (fun i ↦ comap (f i) (l i)) = comap (Pi.map f) (pi l) := by
  simp [Filter.pi, Filter.comap_comap, Function.comp_def]

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