English
If ι is nontrivial, then for each i the coordinate function b.coord i : P → k is surjective.
Русский
Если ι непустое, то для каждого i функция coord_i : P → k сюръективна.
LaTeX
$$$\\text{Surjective} (b.coord\\, i)$$$
Lean4
theorem surjective_coord [Nontrivial ι] (i : ι) : Function.Surjective <| b.coord i := by
classical
intro x
obtain ⟨j, hij⟩ := exists_ne i
let s : Finset ι := { i, j }
have hi : i ∈ s := by simp [s]
let w : ι → k := fun j' => if j' = i then x else 1 - x
have hw : s.sum w = 1 := by
simp [s, w, Finset.sum_ite, Finset.filter_insert, hij, Finset.filter_true_of_mem, Finset.filter_false_of_mem]
use s.affineCombination k b w
simp [w, b.coord_apply_combination_of_mem hi hw]