prod_assoc_symm_preimage — Mathlib

English

Let s ⊆ α, t ⊆ β, u ⊆ γ. Then the preimage under the inverse associativity of (s × t) × u equals s × t × u.

Русский

Пусть 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

@[simp]
theorem prod_assoc_symm_preimage {α β γ} {s : Set α} {t : Set β} {u : Set γ} :
    (Equiv.prodAssoc α β γ).symm ⁻¹' (s ×ˢ t) ×ˢ u = s ×ˢ t ×ˢ u :=
  by
  ext
  simp [and_assoc]
    -- `@[simp]` doesn't like these lemmas, as it uses `Set.image_congr'` to turn `Equiv.prodAssoc`
    -- into a lambda expression and then unfold it.

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