smul_mem_of_zero_mem — Mathlib

English

If s is strictly convex and 0 ∈ s, and x ∈ s with x ≠ 0, then t • x ∈ interior s for 0 < t < 1.

Русский

Если s строго выпукло и 0 ∈ s, и x ∈ s при x ≠ 0, то для 0 < t < 1 точка t • x лежит во внутренности s.

LaTeX

$$$\StrictConvex 𝕜 s \rightarrow 0 \in s \rightarrow x \in s \rightarrow x \neq 0 \rightarrow \forall t \in (0,1),\; t \cdot x \in interior s$$$

Lean4

theorem smul_mem_of_zero_mem [AddRightStrictMono 𝕜] (hs : StrictConvex 𝕜 s) (zero_mem : (0 : E) ∈ s) (hx : x ∈ s)
    (hx₀ : x ≠ 0) {t : 𝕜} (ht₀ : 0 < t) (ht₁ : t < 1) : t • x ∈ interior s := by
  simpa using hs.add_smul_mem zero_mem (by simpa using hx) hx₀ ht₀ ht₁

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