trans_toContinuousAffineMap — Mathlib

English

Relates the trans operation to the corresponding continuous affine maps.

Русский

Связь операции trans с соответствующими непрерывными аффинными отображениями.

LaTeX

$$$ (e : P_1 \to P_2).trans (e' : P_2 \to P_3) : P_1 \to P_3$$$

Lean4

theorem trans_toContinuousAffineMap (e : P₁ ≃ᴬ[k] P₂) (e' : P₂ ≃ᴬ[k] P₃) :
    (e.trans e').toContinuousAffineMap = e'.toContinuousAffineMap.comp e.toContinuousAffineMap :=
  rfl

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