English
The positive tangent cone at a is the set of all limits of c_n d_n with c_n → ∞ and a + d_n ∈ s eventually.
Русский
Положительный касательный конус в точке a — это множество всех пределов последовательностей c_n d_n с c_n → ∞ и с тем, что a + d_n рано постоянно лежит в s.
LaTeX
$$$ posTangentConeAt(s,a) = \\{ y \\in E \\mid \\exists (c_n),(d_n): \\forall^\\infty n, a+d_n \\in s \\wedge \\ Tendsto c_n \\to \\infty, \\ Tendsto (c_n d_n) \\to y \\}$$$
Lean4
/-- "Positive" tangent cone to `s` at `x`; the only difference from `tangentConeAt`
is that we require `c n → ∞` instead of `‖c n‖ → ∞`. One can think about `posTangentConeAt`
as `tangentConeAt NNReal` but we have no theory of normed semifields yet. -/
def posTangentConeAt (s : Set E) (x : E) : Set E :=
{y : E |
∃ (c : ℕ → ℝ) (d : ℕ → E),
(∀ᶠ n in atTop, x + d n ∈ s) ∧ Tendsto c atTop atTop ∧ Tendsto (fun n => c n • d n) atTop (𝓝 y)}
