English
A four-way product map rearrangement: map of a rearranged product equals product of rearranged factors.
Русский
Преобразование четырехфакторного произведения: отображение перестановки приводит к перестановке соответствующих факторов.
LaTeX
$$$\mathrm{map}\ (\lambda p : (\alpha \times \beta) \times \gamma \times \delta \;\Rightarrow ((p.1.1, p.2.1), (p.1.2, p.2.2)))\ ((f \times\! g) \times\! (h \times\! k)) = (f \times\! h) \times\! (g \times\! k)$$$
Lean4
/-- A useful lemma when dealing with uniformities. -/
theorem map_swap4_prod {h : Filter γ} {k : Filter δ} :
map (fun p : (α × β) × γ × δ => ((p.1.1, p.2.1), (p.1.2, p.2.2))) ((f ×ˢ g) ×ˢ (h ×ˢ k)) = (f ×ˢ h) ×ˢ (g ×ˢ k) :=
by simp_rw [map_swap4_eq_comap, prod_eq_inf, comap_inf, comap_comap]; ac_rfl
