combo_self_interior_subset_interior

English

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

Русский

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

LaTeX

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

Lean4

/-- If `s` is a convex set, then `a • s + b • interior s ⊆ interior s` for all `0 ≤ a`, `0 < b`,
`a + b = 1`. See also `Convex.combo_closure_interior_subset_interior` for a stronger version. -/
theorem combo_self_interior_subset_interior {s : Set E} (hs : Convex 𝕜 s) {a b : 𝕜} (ha : 0 ≤ a) (hb : 0 < b)
    (hab : a + b = 1) : a • s + b • interior s ⊆ interior s :=
  by
  rw [add_comm]
  exact hs.combo_interior_self_subset_interior hb ha (add_comm a b ▸ hab)

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