affineCombination_mem_interior_face_iff_mem_Ioo

English

Interior membership with positive weights on face iff all positive on those indices.

Русский

Принадлежность interior при положительных весах по грани эквивалентна положительности весов на соответствующих индексах.

LaTeX

$$$ (w_i > 0) \text{ on } fs \quad \land \text{others zero} \Rightarrow \text{interior holds}$$$

Lean4

theorem affineCombination_mem_interior_face_iff_mem_Ioo {n : ℕ} (s : Simplex k P n) {fs : Finset (Fin (n + 1))} {m : ℕ}
    (h : #fs = m + 1) {w : Fin (n + 1) → k} (hw : ∑ i, w i = 1) :
    Finset.univ.affineCombination k s.points w ∈ (s.face h).interior ↔
      (∀ i ∈ fs, w i ∈ Set.Ioo 0 1) ∧ (∀ i ∉ fs, w i = 0) :=
  affineCombination_mem_setInterior_face_iff_mem _ _ _ hw

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