lineMap_mem — Mathlib

English

If p0 and p1 lie in an affine subspace Q, then every point on the line through p0 and p1 lies in Q as well, for all parameter c.

Русский

Если точки p0 и p1 принадлежат Q, то каждая точка на линии через p0 и p1 принадлежит Q при любом параметре c.

LaTeX

$$$ c \\\\in k \\,\\\\Rightarrow \\\\lineMap p_0 p_1 c \\\\in Q $$$

Lean4

theorem lineMap_mem {k V P : Type*} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] {Q : AffineSubspace k P}
    {p₀ p₁ : P} (c : k) (h₀ : p₀ ∈ Q) (h₁ : p₁ ∈ Q) : AffineMap.lineMap p₀ p₁ c ∈ Q :=
  by
  rw [AffineMap.lineMap_apply]
  exact Q.smul_vsub_vadd_mem c h₁ h₀ h₀

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