combo_closure_interior_mem_interior

English

If s is convex and a,b satisfy a ≥ 0, b ≥ 0 and a + b = 1, then a · closure(s) + b · interior(s) ⊆ interior(s).

Русский

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

LaTeX

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

Lean4

theorem combo_closure_interior_mem_interior {s : Set E} (hs : Convex 𝕜 s) {x y : E} (hx : x ∈ closure s)
    (hy : y ∈ interior s) {a b : 𝕜} (ha : 0 ≤ a) (hb : 0 < b) (hab : a + b = 1) : a • x + b • y ∈ interior s :=
  hs.combo_closure_interior_subset_interior ha hb hab <| add_mem_add (smul_mem_smul_set hx) (smul_mem_smul_set hy)

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