toContinuousAffineMap_toAffineMap

English

The affine map underlying the continuous affine map of e coincides with the affine map coming from e as an affine equivalence.

Русский

Базовая аффинная карта непрерывной аффинной карты e совпадает с аффинной картой, полученной из e как аффинного эквивалента.

LaTeX

$$$e.toContinuousAffineMap.toAffineMap = e.toAffineEquiv.toAffineMap$$$

Lean4

theorem toContinuousAffineMap_toAffineMap (e : P₁ ≃ᴬ[k] P₂) :
    e.toContinuousAffineMap.toAffineMap = e.toAffineEquiv.toAffineMap :=
  rfl

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