English
If there exists r ≠ 0 with |r|<1 such that x+r^n y ∈ s for all large n, then y lies in the tangent cone to s at x.
Русский
Если существует число r с r ≠ 0 и |r|<1, и x+ r^n y ∈ s для больших n, то направление y принадлежит касательному конусу к s в точке x.
LaTeX
$$$\text{If } ∃ r\neq 0,\ |r|<1,\ hs:\forall\text{ sufficiently large }n:\ x+ r^n y\in s, \ then\ y\in tangentConeAt 𝕜 s x.$$$
Lean4
theorem mem_tangentConeAt_of_pow_smul {r : 𝕜} (hr₀ : r ≠ 0) (hr : ‖r‖ < 1) (hs : ∀ᶠ n : ℕ in atTop, x + r ^ n • y ∈ s) :
y ∈ tangentConeAt 𝕜 s x := by
refine ⟨fun n ↦ (r ^ n)⁻¹, fun n ↦ r ^ n • y, hs, ?_, ?_⟩
· simp only [norm_inv, norm_pow, ← inv_pow]
exact tendsto_pow_atTop_atTop_of_one_lt <| (one_lt_inv₀ (norm_pos_iff.2 hr₀)).2 hr
· simp only [inv_smul_smul₀ (pow_ne_zero _ hr₀), tendsto_const_nhds]
