prod_assoc — Mathlib

English

The product is associative up to a natural equivalence: map (prodAssoc) ((f × g) × h) = f × (g × h).

Русский

Произведение ассоциативно через естественное равенство: map(prodAssoc)((f × g) × h) = f × (g × h).

LaTeX

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

Lean4

theorem prod_assoc (f : Filter α) (g : Filter β) (h : Filter γ) :
    map (Equiv.prodAssoc α β γ) ((f ×ˢ g) ×ˢ h) = f ×ˢ (g ×ˢ h) := by
  simp_rw [← comap_equiv_symm, prod_eq_inf, comap_inf, comap_comap, inf_assoc, Function.comp_def,
    Equiv.prodAssoc_symm_apply]

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