affineCombination_mem_closedInterior_face_iff_mem_Icc

English

Closed interior membership corresponds to weights lying in the closed interval [0,1] for indices in the face and zeros outside.

Русский

Принадлежность к закрытой внутренности соответствует весам в интервале [0,1] для индексов лица и нулям вне лица.

LaTeX

$$$ (w_i \in [0,1] \text{ for } i \in fs) \land (w_i = 0 \text{ for } i \notin fs) \Rightarrow \text{membership}$$$

Lean4

theorem affineCombination_mem_closedInterior_face_iff_mem_Icc {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).closedInterior ↔
      (∀ i ∈ fs, w i ∈ Set.Icc 0 1) ∧ (∀ i ∉ fs, w i = 0) :=
  affineCombination_mem_setInterior_face_iff_mem _ _ _ hw

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