add_smul_mem_interior' — Mathlib

English

If s is convex, x ∈ closure s, y ∈ interior s, then x + t y ∈ interior s for t ∈ (0,1].

Русский

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

LaTeX

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

Lean4

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

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