English
If s is strictly convex and x ∈ s, x+y ∈ s with y ≠ 0, then for t ∈ (0,1) the point x + t y lies in interior s.
Русский
Если s строго выпукло и x ∈ s, x+y ∈ s с y ≠ 0, то при t ∈ (0,1) точка x + t y лежит во внутренности s.
LaTeX
$$$\StrictConvex 𝕜 s \rightarrow x \in s \rightarrow (x + y) \in s \rightarrow y \neq 0 \rightarrow \forall t \in (0,1),\; x + t y \in interior s$$$
Lean4
theorem add_smul_mem [AddRightStrictMono 𝕜] (hs : StrictConvex 𝕜 s) (hx : x ∈ s) (hxy : x + y ∈ s) (hy : y ≠ 0) {t : 𝕜}
(ht₀ : 0 < t) (ht₁ : t < 1) : x + t • y ∈ interior s :=
by
have h : x + t • y = (1 - t) • x + t • (x + y) := by match_scalars <;> simp
rw [h]
exact
hs hx hxy (fun h => hy <| add_left_cancel (a := x) (by rw [← h, add_zero])) (sub_pos_of_lt ht₁) ht₀
(sub_add_cancel 1 t)
