prod_assoc_preimage — Mathlib

English

Let s ⊆ α, t ⊆ β, u ⊆ γ. Then the preimage of s × t × u under the associativity bijection equals (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_preimage {α β γ} {s : Set α} {t : Set β} {u : Set γ} :
    Equiv.prodAssoc α β γ ⁻¹' s ×ˢ t ×ˢ u = (s ×ˢ t) ×ˢ u :=
  by
  ext
  simp [and_assoc]

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