combo_self_interior_mem_interior — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem combo_self_interior_mem_interior {s : Set E} (hs : Convex 𝕜 s) {x y : E} (hx : x ∈ 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_mem_interior (subset_closure hx) hy ha hb hab

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