English
If an open segment is contained in s, then the direction y − x belongs to tangentConeAt(s, x).
Русский
Если открытый отрезок содержится в s, то направление y − x принадлежит tangentConeAt(s, x).
LaTeX
$$$ (\\mathrm{openSegment}\\; \\mathbb{R}\\; x\\; y) \\subseteq s \\;\Rightarrow\; y - x \\in \\operatorname{tangentCone}_{\\mathbb{R}}(s, x) $$$
Lean4
/-- If a subset of a real vector space contains an open segment, then the direction of this
segment belongs to the tangent cone at its endpoints. -/
theorem mem_tangentConeAt_of_openSegment_subset {s : Set G} {x y : G} (h : openSegment ℝ x y ⊆ s) :
y - x ∈ tangentConeAt ℝ s x :=
by
refine mem_tangentConeAt_of_pow_smul one_half_pos.ne' (by norm_num) ?_
refine (eventually_ne_atTop 0).mono fun n hn ↦ (h ?_)
rw [openSegment_eq_image]
refine ⟨(1 / 2) ^ n, ⟨?_, ?_⟩, ?_⟩
· exact pow_pos one_half_pos _
· exact pow_lt_one₀ one_half_pos.le one_half_lt_one hn
· simp only [sub_smul, one_smul, smul_sub]; abel
