English
Mapping via projections distributes over products: map m1 f1 × map m2 f2 = map (λ p, (m1 p.1, m2 p.2)) (f1 × f2).
Русский
Отображение через проекции распределяется по произведениям: map m1 f1 × map m2 f2 = map (λ p, (m1 p.1, m2 p.2)) (f1 × f2).
LaTeX
$$$\mathrm{map}\ m_1\ f_1 \times\! \mathrm{map}\ m_2\ f_2 = \mathrm{map}\ (\lambda p : \alpha_1 \times \alpha_2 \mapsto (m_1 p.1, m_2 p.2))\ (f_1 \times\! f_2)$$$
Lean4
theorem prod_map_map_eq.{u, v, w, x} {α₁ : Type u} {α₂ : Type v} {β₁ : Type w} {β₂ : Type x} {f₁ : Filter α₁}
{f₂ : Filter α₂} {m₁ : α₁ → β₁} {m₂ : α₂ → β₂} :
map m₁ f₁ ×ˢ map m₂ f₂ = map (fun p : α₁ × α₂ => (m₁ p.1, m₂ p.2)) (f₁ ×ˢ f₂) :=
le_antisymm
(fun s hs =>
let ⟨s₁, hs₁, s₂, hs₂, h⟩ := mem_prod_iff.mp hs
mem_of_superset (prod_mem_prod (image_mem_map hs₁) (image_mem_map hs₂)) <| by
rwa [prod_image_image_eq, image_subset_iff])
((tendsto_map.comp tendsto_fst).prodMk (tendsto_map.comp tendsto_snd))
