prod_assoc_image — Mathlib

English

The image of the triple product (s × t) × u under the associativity bijection equals the triple product s × t × u.

Русский

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

LaTeX

$$$ \mathrm{Equiv.prodAssoc}\''( (s \times t) \times u) = s \times t \times u $$$

Lean4

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

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