English
If s is convex, and a,b are scalars with a > 0, b ≥ 0 and a + b = 1, then a · interior(s) + b · s ⊆ interior(s).
Русский
Пусть S выпукло и a,b удовлетворяют a > 0, b ≥ 0, a + b = 1. Тогда a·int(S) + b·S ⊆ int(S).
LaTeX
$$$$a\cdot \operatorname{Int}(s) + b\cdot s \subseteq \operatorname{Int}(s),\quad a>0,\; b\ge 0,\; a+b=1.$$$$
Lean4
/-- If `s` is a convex set, then `a • interior s + b • s ⊆ interior s` for all `0 < a`, `0 ≤ b`,
`a + b = 1`. See also `Convex.combo_interior_closure_subset_interior` for a stronger version. -/
theorem combo_interior_self_subset_interior {s : Set E} (hs : Convex 𝕜 s) {a b : 𝕜} (ha : 0 < a) (hb : 0 ≤ b)
(hab : a + b = 1) : a • interior s + b • s ⊆ interior s :=
calc
a • interior s + b • s ⊆ a • interior s + b • closure s := add_subset_add Subset.rfl <| image_mono subset_closure
_ ⊆ interior s := hs.combo_interior_closure_subset_interior ha hb hab
