English
If the index set ι is a subsingleton, then every coordinate function is the constant map to 1; i.e., coord_i is the constant function 1.
Русский
Если множество индексов ι субединственно, каждая координатная функция равна константе 1; то есть coord_i ≡ 1.
LaTeX
$$$\\text{If } ι \\text{ is subsingleton, then } (b.coord\\, i) = 1 \\text{ as a function } P \\to k$$$
Lean4
@[simp]
theorem coe_coord_of_subsingleton_eq_one [Subsingleton ι] (i : ι) : (b.coord i : P → k) = 1 :=
by
ext q
have hp : (range b).Subsingleton := by
rw [← image_univ]
apply Subsingleton.image
apply subsingleton_of_subsingleton
haveI := AffineSubspace.subsingleton_of_subsingleton_span_eq_top hp b.tot
let s : Finset ι := { i }
have hi : i ∈ s := by simp [s]
have hw : s.sum (Function.const ι (1 : k)) = 1 := by simp [s]
have hq : q = s.affineCombination k b (Function.const ι (1 : k)) := by simp [eq_iff_true_of_subsingleton]
rw [Pi.one_apply, hq, b.coord_apply_combination_of_mem hi hw, Function.const_apply]
