prodCongr — Mathlib

English

If e₁: P₁ ≃ᴬ[k] P₂ and e₂: P₃ ≃ᴬ[k] P₄ are continuous affine equivalences, then their product e₁.prodCongr e₂ gives a continuous affine equivalence (P₁ × P₃) ≃ᴬ[k] (P₂ × P₄).

Русский

Если e₁: P₁ ≃ᴬ[k] P₂ и e₂: P₃ ≃ᴬ[k] P₄ — непрерывные аффинные эквивалентности, то их произведение e₁.prodCongr e₂ задаёт непрерывную аффинную эквивалентность (P₁ × P₃) ≃ᴬ[k] (P₂ × P₄).

LaTeX

$$$\text{prodCongr}(e_1,e_2) : P_1 \times P_3 \;\simeq_ᴬ[k]\; P_2 \times P_4.$$$

Lean4

/-- Product of two continuous affine equivalences. The map comes from `Equiv.prodCongr` -/
@[simps toAffineEquiv]
def prodCongr : P₁ × P₃ ≃ᴬ[k] P₂ × P₄ where
  __ := AffineEquiv.prodCongr e₁ e₂
  continuous_toFun := by eta_expand; dsimp; fun_prop
  continuous_invFun := by eta_expand; dsimp; fun_prop

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