tendsto_prodAssoc_symm — Mathlib

English

Symmetric tendsto for prodAssoc: Tendsto (prodAssoc).symm ((f × (g × h))) ((f × g) × h).

Русский

Симметричная тонкая формула предельности для prodAssoc: Tendsto (prodAssoc).symm ((f × (g × h))) ((f × g) × h).

LaTeX

$$$\mathrm{Tendsto}\ (\mathrm{Equiv.prodAssoc}).\mathrm{symm}\ (f \times\! (g \times\! h))\ (f \times\! g) \times\! h$$$

Lean4

theorem tendsto_prodAssoc_symm {h : Filter γ} : Tendsto (Equiv.prodAssoc α β γ).symm (f ×ˢ (g ×ˢ h)) ((f ×ˢ g) ×ˢ h) :=
  (prod_assoc_symm f g h).le

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