English
If s is convex and a,b are scalars with a > 0, b ≥ 0 and a + b = 1, then a · interior(s) + b · closure(s) ⊆ interior(s).
Русский
Пусть S выпукло, и скаляры a,b удовлетворяют a > 0, b ≥ 0 и a + b = 1. Тогда a·int(S) + b·cl(S) ⊆ int(S).
LaTeX
$$$$a\cdot \operatorname{Int}(s) + b\cdot \overline{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 • closure s ⊆ interior s` for all `0 < a`,
`0 ≤ b`, `a + b = 1`. See also `Convex.combo_interior_self_subset_interior` for a weaker version. -/
theorem combo_interior_closure_subset_interior {s : Set E} (hs : Convex 𝕜 s) {a b : 𝕜} (ha : 0 < a) (hb : 0 ≤ b)
(hab : a + b = 1) : a • interior s + b • closure s ⊆ interior s :=
interior_smul₀ ha.ne' s ▸
calc
interior (a • s) + b • closure s ⊆ interior (a • s) + closure (b • s) :=
add_subset_add Subset.rfl (smul_closure_subset b s)
_ = interior (a • s) + b • s := by rw [isOpen_interior.add_closure (b • s)]
_ ⊆ interior (a • s + b • s) := subset_interior_add_left
_ ⊆ interior s := interior_mono <| hs.set_combo_subset ha.le hb hab
