add_smul_mem_interior — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

/-- If `x ∈ s` and `x + y ∈ interior s`, then `x + t y ∈ interior s` for `t ∈ (0, 1]`. -/
theorem add_smul_mem_interior {s : Set E} (hs : Convex 𝕜 s) {x y : E} (hx : x ∈ s) (hy : x + y ∈ interior s) {t : 𝕜}
    (ht : t ∈ Ioc (0 : 𝕜) 1) : x + t • y ∈ interior s :=
  hs.add_smul_mem_interior' (subset_closure hx) hy ht

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