closedInterior — Mathlib

English

Analogous to interior, but for closed interior weights lie in [0,1].

Русский

Аналогично interior, но для закрытой внутренности веса лежат в [0,1].

LaTeX

$$$ Finset.univ.affineCombination k s.points w \in (s.face h).closedInterior \iff (∀ i ∈ fs, w_i ∈ [0,1]) ∧ (∀ i ∉ fs, w_i = 0) $$$

Lean4

/-- `s.closedInterior` is the set of points that can be expressed as an affine combination
of the vertices with weights between 0 and 1 inclusive. This is equivalent to the convex hull of
the vertices or the closure of the interior. -/
protected def closedInterior {n : ℕ} (s : Simplex k P n) : Set P :=
  s.setInterior (Set.Icc 0 1)

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