affineCombination_mem_setInterior_iff

English

An affine combination belongs to the interior of a face iff all included weights lie in (0,1) and weights outside the face vanish.

Русский

Аффинное сочетание принадлежит interior грани тогда, когда все веса внутри множества лежат в (0,1), а веса вне множества равны нулю.

LaTeX

$$$ Finset.univ.affineCombination k s.points w \in (s.face h).interior \iff (\forall i \in fs, 0 < w_i) \land (\forall i \notin fs, w_i = 0) $$$

Lean4

theorem affineCombination_mem_setInterior_iff {I : Set k} {n : ℕ} {s : Simplex k P n} {w : Fin (n + 1) → k}
    (hw : ∑ i, w i = 1) : Finset.univ.affineCombination k s.points w ∈ s.setInterior I ↔ ∀ i, w i ∈ I :=
  by
  refine ⟨fun ⟨w', hw', hw'01, hww'⟩ ↦ ?_, fun h ↦ ⟨w, hw, h, rfl⟩⟩
  simp_rw [← (affineIndependent_iff_eq_of_fintype_affineCombination_eq k s.points).1 s.independent w' w hw' hw hww']
  exact hw'01

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