English
Finite-type version of indicator extension: the indicator equality holds for univ and affine combinations under a finite embedding.
Русский
Конечная версия: равенство индикаторов сохраняется при переходе через вложение на универсе.
LaTeX
$$$\\operatorname{AffineIndependent} k p \\Rightarrow \\forall {w_1,w_2},\\; (\\sum_{i} w_1 i =1) \\land (\\sum_{i} w_2 i =1) \\rightarrow \\exists e:\\iota_2\\hookrightarrow\\iota,\\; \\text{indicator equality}$$$
Lean4
theorem indicator_extend_eq_of_affineCombination_comp_embedding_eq_of_fintype [Fintype ι] {ι₂ : Type*} [Fintype ι₂]
{p : ι → P} (ha : AffineIndependent k p) {w₁ : ι → k} {w₂ : ι₂ → k} (hw₁ : ∑ i, w₁ i = 1) (hw₂ : ∑ i, w₂ i = 1)
(e : ι₂ ↪ ι) (h : Finset.univ.affineCombination k (p ∘ e) w₂ = Finset.univ.affineCombination k p w₁) :
Set.indicator (Set.range e) (extend e w₂ 0) = w₁ := by
simpa using ha.indicator_extend_eq_of_affineCombination_comp_embedding_eq hw₁ hw₂ e h
