comap_prod — Mathlib

English

For f : α → β, g : γ → δ, lb ∈ Filter β, ld ∈ Filter δ, comap (Prod.map f g) (lb ×ˢ ld) equals comap f lb ×ˢ comap g ld.

Русский

Для отображений f: α → β и g: γ → δ, предобраз через Pro map умножения равен произведению предобразов.

LaTeX

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

Lean4

theorem comap_prod (f : α → β × γ) (b : Filter β) (c : Filter γ) :
    comap f (b ×ˢ c) = comap (Prod.fst ∘ f) b ⊓ comap (Prod.snd ∘ f) c := by
  rw [prod_eq_inf, comap_inf, Filter.comap_comap, Filter.comap_comap]

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