combo_interior_self_mem_interior — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem combo_interior_self_mem_interior {s : Set E} (hs : Convex 𝕜 s) {x y : E} (hx : x ∈ interior s) (hy : y ∈ s)
    {a b : 𝕜} (ha : 0 < a) (hb : 0 ≤ b) (hab : a + b = 1) : a • x + b • y ∈ interior s :=
  hs.combo_interior_closure_mem_interior hx (subset_closure hy) ha hb hab

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