coe_toContinuousAffineMap — Mathlib

English

If e is a continuous affine equivalence between P1 and P2, then the underlying function of its associated continuous affine map is exactly e.

Русский

Пусть e является непрерывным аффинным эквивалентом между P1 и P2. Тогда базовая функция сопутствующей непрерывной аффинной карты совпадает с e.

LaTeX

$$$\\forall x\\in P_1\\ ,\\ (\mathrm{toContinuousAffineMap}(e))(x) = e(x)$$$

Lean4

@[simp]
theorem coe_toContinuousAffineMap (e : P₁ ≃ᴬ[k] P₂) : ⇑e.toContinuousAffineMap = e :=
  rfl

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