English
For a fixed index i, the vectors b j −ᵥ b i (for j ≠ i) form a linear basis of the model space V.
Русский
Для фиксированного индекса i векторное множество {b_j −ᵥ b_i} (при j ≠ i) образуют базис модели V.
LaTeX
$$basisOf i = Basis { j : ι \ { i } } k V with (b j −ᵥ b i) as elements$$
Lean4
/-- Given an affine basis for an affine space `P`, if we single out one member of the family, we
obtain a linear basis for the model space `V`.
The linear basis corresponding to the singled-out member `i : ι` is indexed by `{j : ι // j ≠ i}`
and its `j`th element is `b j -ᵥ b i`. (See `basisOf_apply`.) -/
noncomputable def basisOf (i : ι) : Basis { j : ι // j ≠ i } k V :=
Basis.mk ((affineIndependent_iff_linearIndependent_vsub k b i).mp b.ind)
(by
suffices Submodule.span k (range fun j : { x // x ≠ i } => b ↑j -ᵥ b i) = vectorSpan k (range b) by
rw [this, ← direction_affineSpan, b.tot, AffineSubspace.direction_top]
conv_rhs => rw [← image_univ]
rw [vectorSpan_image_eq_span_vsub_set_right_ne k b (mem_univ i)]
congr
ext v
simp)
