English
If the segment x to y lies in s, then the vector y − x belongs to posTangentConeAt s x.
Русский
Если отрезок x до y лежит в s, то вектор y − x принадлежит posTangentConeAt s x.
LaTeX
$$$(x,y)\\text{ segment subset } s \\Rightarrow y-x \\in posTangentConeAt(s,x)$$$
Lean4
/-- If `[x -[ℝ] x + y] ⊆ s`, then `y` belongs to the positive tangent cone of `s`.
Before 2024-07-13, this lemma used to be called `mem_posTangentConeAt_of_segment_subset`.
See also `sub_mem_posTangentConeAt_of_segment_subset`
for the lemma that used to be called `mem_posTangentConeAt_of_segment_subset`. -/
theorem mem_posTangentConeAt_of_segment_subset (h : [x -[ℝ] x + y] ⊆ s) : y ∈ posTangentConeAt s x :=
by
refine mem_posTangentConeAt_of_frequently_mem (Eventually.frequently ?_)
rw [eventually_nhdsWithin_iff]
filter_upwards [ge_mem_nhds one_pos] with t ht₁ ht₀
apply h
rw [segment_eq_image', add_sub_cancel_left]
exact mem_image_of_mem _ ⟨le_of_lt ht₀, ht₁⟩
