English
If a vector y is frequently along a direction such that x + t y ∈ s, then y ∈ posTangentConeAt s x.
Русский
Если вектор y часто встречается так, что x + t y ∈ s, то y принадлежит posTangentConeAt(s,x).
LaTeX
$$$\\text{Frequent}(t\\mapsto x+t y) \\Rightarrow y \\in posTangentConeAt(s,x)$$$
Lean4
theorem mem_posTangentConeAt_of_frequently_mem (h : ∃ᶠ t : ℝ in 𝓝[>] 0, x + t • y ∈ s) : y ∈ posTangentConeAt s x :=
by
obtain ⟨a, ha, has⟩ := Filter.exists_seq_forall_of_frequently h
refine ⟨a⁻¹, (a · • y), Eventually.of_forall has, tendsto_inv_nhdsGT_zero.comp ha, ?_⟩
refine tendsto_const_nhds.congr' ?_
filter_upwards [(tendsto_nhdsWithin_iff.1 ha).2] with n (hn : 0 < a n)
simp [ne_of_gt hn]