English
The product of two comaps equals the comap along the product map of the product filters.
Русский
Произведение сопряжений равно сопряжению по произведению отображения от произведения фильтров к произведению фильтров.
LaTeX
$$$\mathrm{comap}\, m_1\, f_1 \times\mathrm{comap}\, m_2\, f_2 = \mathrm{comap}\,\bigl(\lambda p : \beta_1 \times \beta_2\;\mapsto (m_1\, p.1,\, m_2\, p.2)\bigr) (f_1 \times f_2)$$$
Lean4
theorem prod_comap_comap_eq.{u, v, w, x} {α₁ : Type u} {α₂ : Type v} {β₁ : Type w} {β₂ : Type x} {f₁ : Filter α₁}
{f₂ : Filter α₂} {m₁ : β₁ → α₁} {m₂ : β₂ → α₂} :
comap m₁ f₁ ×ˢ comap m₂ f₂ = comap (fun p : β₁ × β₂ => (m₁ p.1, m₂ p.2)) (f₁ ×ˢ f₂) := by
simp only [prod_eq_inf, comap_comap, comap_inf, Function.comp_def]
