lineMap — Mathlib

English

There is a canonical affine map lineMap: R → P sending t to p0 + t(p1 − p0).

Русский

Существует каноническая аффинная карта lineMap: R → P, отправляющая t в p0 + t(p1 − p0).

LaTeX

$$$\text{lineMap}(p_0,p_1): R \toᴬ[R] P$$$

Lean4

/-- The continuous affine map sending `0` to `p₀` and `1` to `p₁` -/
def lineMap (p₀ p₁ : P) [TopologicalSpace R] [TopologicalSpace V] [ContinuousSMul R V] [ContinuousVAdd V P] : R →ᴬ[R] P
    where
  toAffineMap := AffineMap.lineMap p₀ p₁
  cont := (continuous_id.smul continuous_const).vadd continuous_const

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