add_smul_sub_mem — Mathlib

English

If s is strictly convex and 0 ∈ s, x ∈ s with x ≠ 0, then for any t > 1 we have x ∈ t · interior s.

Русский

Если s строго выпукло, 0 ∈ s, x ∈ s и x ≠ 0, то для любого t > 1 выполняется x ∈ t · interior s.

LaTeX

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

Lean4

theorem add_smul_sub_mem [AddRightMono 𝕜] (h : StrictConvex 𝕜 s) (hx : x ∈ s) (hy : y ∈ s) (hxy : x ≠ y) {t : 𝕜}
    (ht₀ : 0 < t) (ht₁ : t < 1) : x + t • (y - x) ∈ interior s :=
  by
  apply h.openSegment_subset hx hy hxy
  rw [openSegment_eq_image']
  exact mem_image_of_mem _ ⟨ht₀, ht₁⟩

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