prodAssoc — Mathlib

English

For p = (p₁, p₃), (e₁.prodCongr e₂) p = (e₁ p₁, e₂ p₃).

Русский

Для p = (p₁, p₃) выполняется (e₁.prodCongr e₂) p = (e₁ p₁, e₂ p₃).

LaTeX

$$$ (e_1.prodCongr e_2) \; p = (e_1(p_1), e_2(p_3)). $$$

Lean4

/-- Product of affine spaces is associative up to continuous affine isomorphism. -/
@[simps! apply symm_apply toAffineEquiv]
def prodAssoc : (P₁ × P₂) × P₃ ≃ᴬ[k] P₁ × (P₂ × P₃)
    where
  __ := AffineEquiv.prodAssoc k P₁ P₂ P₃
  continuous_toFun := by eta_expand; dsimp; fun_prop
  continuous_invFun := by eta_expand; dsimp; fun_prop

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