surjective_coord — Mathlib

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]

Похожие утверждения