English
If s is convex, then a · interior(s) + b · closure(s) ⊆ interior(s) whenever hx ∈ interior(s) and hy ∈ closure(s) and a,b ≥ 0 with a + b = 1, in the sense of points x and y chosen from interior and closure respectively.
Русский
Если S выпукло, то a·int(S) + b·closure(S) ⊆ int(S) при выборе точек из interior и closure соответственно и a,b ≥ 0 с a+b=1.
LaTeX
$$$$a\cdot \operatorname{Int}(s) + b\cdot \overline{s} \subseteq \operatorname{Int}(s)\quad\text{under } a,b\ge 0,\; a+b=1.$$$$
Lean4
theorem combo_interior_closure_mem_interior {s : Set E} (hs : Convex 𝕜 s) {x y : E} (hx : x ∈ interior s)
(hy : y ∈ closure s) {a b : 𝕜} (ha : 0 < a) (hb : 0 ≤ b) (hab : a + b = 1) : a • x + b • y ∈ interior s :=
hs.combo_interior_closure_subset_interior ha hb hab <| add_mem_add (smul_mem_smul_set hx) (smul_mem_smul_set hy)
