add_smul_sub_mem_interior' — Mathlib

English

If s is convex, x ∈ closure s, y ∈ interior s, and t ∈ (0,1), then x + t(y - x) ∈ interior s.

Русский

Если S выпукло, x ∈ closure(S), y ∈ interior(S), и t ∈ (0,1), то x + t(y - x) ∈ interior(S).

LaTeX

$$$$x + t\cdot (y - x) \in \operatorname{Int}(s),\quad t \in (0,1).$$$$

Lean4

/-- If `x ∈ closure s` and `y ∈ interior s`, then the segment `(x, y]` is included in `interior s`.
-/
theorem add_smul_sub_mem_interior' {s : Set E} (hs : Convex 𝕜 s) {x y : E} (hx : x ∈ closure s) (hy : y ∈ interior s)
    {t : 𝕜} (ht : t ∈ Ioc (0 : 𝕜) 1) : x + t • (y - x) ∈ interior s := by
  simpa only [sub_smul, smul_sub, one_smul, add_sub, add_comm] using
    hs.combo_interior_closure_mem_interior hy hx ht.1 (sub_nonneg.mpr ht.2) (add_sub_cancel _ _)

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