tendsto_prodAssoc — Mathlib

English

Tendsto of the prodAssoc equivalence: (Equiv.prodAssoc).transforms the product of three filters to the standard grouping.

Русский

Нормализующее свойство предела через prodAssoc: переход через тождество группировки.

LaTeX

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

Lean4

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

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