comap_prodMap_prod — Mathlib

English

Alternative presentation of comap_prodMap_prod with explicit components.

Русский

Альтернативная формулировка comap_prodMap_prod с явными компонентами.

LaTeX

$$$\\mathrm{comap}(\\mathrm{Prod.map} f\\ g) (lb \\timesˢ ld) = (\\mathrm{comap} f\, lb) ×ˢ (\\mathrm{comap} g\, ld)$$$

Lean4

theorem comap_prodMap_prod (f : α → β) (g : γ → δ) (lb : Filter β) (ld : Filter δ) :
    comap (Prod.map f g) (lb ×ˢ ld) = comap f lb ×ˢ comap g ld := by simp [prod_eq_inf, comap_comap, Function.comp_def]

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