tendsto_swap4_prod — Mathlib

English

The Tendsto of the swap4 rearrangement holds for the product of filters.

Русский

Сохранение предельности под перестановкой swap4 в произведении фильтров.

LaTeX

$$$\mathrm{Tendsto}\ (\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

theorem tendsto_swap4_prod {h : Filter γ} {k : Filter δ} :
    Tendsto (fun p : (α × β) × γ × δ => ((p.1.1, p.2.1), (p.1.2, p.2.2))) ((f ×ˢ g) ×ˢ (h ×ˢ k))
      ((f ×ˢ h) ×ˢ (g ×ˢ k)) :=
  map_swap4_prod.le

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