prod_map_map_eq' — Mathlib

English

The same as prod_map_map_eq but with general variables, i.e., map f F × map g G = map (Prod.map f g) (F × G).

Русский

То же самое, что prod_map_map_eq, но с общими переменными: map f F × map g G = map (Prod.map f g) (F × G).

LaTeX

$$$\mathrm{prod\_map\_map\_eq}\ {f,g,F,G}\ :\ \mathrm{map}\ f F \times\! \mathrm{map}\ g G = \mathrm{map}\ (\mathrm{Prod.map}\ f g) (F \times\! G)$$$

Lean4

theorem prod_map_map_eq' {α₁ : Type*} {α₂ : Type*} {β₁ : Type*} {β₂ : Type*} (f : α₁ → α₂) (g : β₁ → β₂) (F : Filter α₁)
    (G : Filter β₁) : map f F ×ˢ map g G = map (Prod.map f g) (F ×ˢ G) :=
  prod_map_map_eq

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