prod_assoc_symm_image — Mathlib

English

The image under the inverse associativity of the triple product equals the triple product: (s × t) × u maps to s × t × u.

Русский

Образ под обратной ассоциативной биекцией тройного произведения равен тройному произведению: (s × t) × u → s × t × u.

LaTeX

$$$ (\mathrm{Equiv.prodAssoc}\, \alpha \ beta \ gamma)^{-1}'' (s \times t \times u) = (s \times t) \times u $$$

Lean4

theorem prod_assoc_symm_image {α β γ} {s : Set α} {t : Set β} {u : Set γ} :
    (Equiv.prodAssoc α β γ).symm '' s ×ˢ t ×ˢ u = (s ×ˢ t) ×ˢ u := by
  simpa only [Equiv.image_eq_preimage] using prod_assoc_preimage

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