Theorems · Theorem · geometry

AffineSubspace.mem_affineSpan_insert_iff

∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] {s : AffineSubspace k P} {p₁ : P},
  p₁ ∈ s → ∀ (p₂ p : P), p ∈ affineSpan k (insert p₂ ↑s) ↔ ∃ r, ∃ p0 ∈ s, p = r • (p₂ -ᵥ p₁) +ᵥ p0

Given a point p₁ in an affine subspace s, and a point p₂, a point p is in the span of s with p₂ added if and only if it is a multiple of p₂ -ᵥ p₁ added to a point in s.

Defined in

Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic

Cited by

3 results in Mathlib

Foundations

Depth 68 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

RingAddCommGroupModuleAddTorsor