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 ∈ interior s.

Русский

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

LaTeX

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

Lean4

/-- If `x ∈ 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 ∈ s) (hy : y ∈ interior s) {t : 𝕜}
    (ht : t ∈ Ioc (0 : 𝕜) 1) : x + t • (y - x) ∈ interior s :=
  hs.add_smul_sub_mem_interior' (subset_closure hx) hy ht

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