prodComm — Mathlib

English

As above, the same equality holds for the continuous affine map underlying the product.

Русский

Как выше, равно выполняется для базовой непрерывной аффинной карты произведения.

LaTeX

$$$ (e_1.prodCongr e_2).toContinuousAffineMap = e_1.toContinuousAffineMap.prodMap e_2.toContinuousAffineMap $$$

Lean4

/-- Product of affine spaces is commutative up to continuous affine isomorphism. -/
@[simps! apply symm_apply toAffineEquiv]
def prodComm : P₁ × P₂ ≃ᴬ[k] P₂ × P₁ where
  __ := AffineEquiv.prodComm k P₁ P₂
  continuous_toFun := continuous_swap
  continuous_invFun := continuous_swap

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