mem_affineSpan_iff_exists — Mathlib

English

A point p lies in the affine span of s iff there exist p1 in s and v in vectorSpan k s with p = v + p1.

Русский

Точка p принадлежит афинному Span множества s тогда и только тогда, когда существуют p1 ∈ s и v ∈ vectorSpan k s такие, что p = v + p1.

LaTeX

$$$p \\in \\operatorname{affineSpan}_k s \\iff \\exists p_1 \\in s, \\exists v \\in \\operatorname{vectorSpan}_k s,\\ p = v +\\!\\! p_1$$$

Lean4

/-- The condition for a point to be in the affine span, in terms of `vectorSpan`. -/
theorem mem_affineSpan_iff_exists {p : P} {s : Set P} :
    p ∈ affineSpan k s ↔ ∃ p₁ ∈ s, ∃ v ∈ vectorSpan k s, p = v +ᵥ p₁ :=
  Iff.rfl

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