affineCombination_mem_closedInterior_iff

English

If weights sum to 1, membership in closed interior of a face is equivalent to nonnegativity on included indices and zeros elsewhere.

Русский

Если веса суммируются до 1, принадлежность к закрытой внутренности грани эквивалентна неотрицательности по включенным индексам и нулям вне их.

LaTeX

$$$ Finset.univ.sum w_i = 1 \Rightarrow (w_i \ge 0 \text{ for } i \in fs) \land (w_i = 0 \text{ for } i \notin fs) \Rightarrow \cdots $$$

Lean4

theorem affineCombination_mem_closedInterior_iff {n : ℕ} {s : Simplex k P n} {w : Fin (n + 1) → k} (hw : ∑ i, w i = 1) :
    Finset.univ.affineCombination k s.points w ∈ s.closedInterior ↔ ∀ i, w i ∈ Set.Icc 0 1 :=
  affineCombination_mem_setInterior_iff hw

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