lineMap_linear — Mathlib

English

If the two lineMap evaluations coincide, then either the endpoints are equal or the scalars are equal.

Русский

Если две оценки lineMap совпадают, то либо концы совпадают, либо параметры совпадают.

LaTeX

$$$ lineMap(p_0,p_1)(c_1) = lineMap(p_0,p_1)(c_2) \iff p_0 = p_1 \ \lor\ c_1 = c_2 $$$

Lean4

@[simp]
theorem lineMap_linear (p₀ p₁ : P1) : (lineMap p₀ p₁ : k →ᵃ[k] P1).linear = LinearMap.id.smulRight (p₁ -ᵥ p₀) :=
  add_zero _

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