combo_closure_interior_subset_interior

English

If s is convex, then a · closure(s) + b · interior(s) ⊆ interior(s) for all a ≥ 0, b > 0 with a + b = 1.

Русский

Если S выпукло, то a·closure(S) + b·int(S) ⊆ int(S) для всех a ≥ 0, b > 0 с a + b = 1.

LaTeX

$$$$a\cdot \overline{s} + b\cdot \operatorname{Int}(s) \subseteq \operatorname{Int}(s),\quad a\ge 0,\; b>0,\; a+b=1.$$$$

Lean4

/-- If `s` is a convex set, then `a • closure s + b • interior s ⊆ interior s` for all `0 ≤ a`,
`0 < b`, `a + b = 1`. See also `Convex.combo_self_interior_subset_interior` for a weaker version. -/
theorem combo_closure_interior_subset_interior {s : Set E} (hs : Convex 𝕜 s) {a b : 𝕜} (ha : 0 ≤ a) (hb : 0 < b)
    (hab : a + b = 1) : a • closure s + b • interior s ⊆ interior s :=
  by
  rw [add_comm]
  exact hs.combo_interior_closure_subset_interior hb ha (add_comm a b ▸ hab)

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