prod_assoc_symm — Mathlib

English

Symmetric form of prod associativity: map (prodAssoc).symm (f × (g × h)) = (f × g) × h.

Русский

Симметричная форма ассоциативности произведения: map(prodAssoc).symm (f × (g × h)) = (f × g) × h.

LaTeX

$$$\mathrm{map}\ (\mathrm{Equiv.prodAssoc}\ \alpha\ \beta\ \gamma).\mathrm{symm}\ (f \times\! (g \times\! h)) = (f \times\! g) \times\! h$$$

Lean4

theorem prod_assoc_symm (f : Filter α) (g : Filter β) (h : Filter γ) :
    map (Equiv.prodAssoc α β γ).symm (f ×ˢ (g ×ˢ h)) = (f ×ˢ g) ×ˢ h := by
  simp_rw [map_equiv_symm, prod_eq_inf, comap_inf, comap_comap, inf_assoc, Function.comp_def, Equiv.prodAssoc_apply]

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