English
If the neighborhoods of x defined by s are contained in those defined by t (in the sense nhdsWithin x s ≤ nhdsWithin x t), then the tangent cone of s at x is contained in the tangent cone of t at x.
Русский
Если окрестности точки x, ограниченные множеством s, содержатся в окрестностях, ограниченных множеством t, то касательный конус к s в x содержится в касательном конусе к t в x.
LaTeX
$$$\\forall x\\in E,\, s,t\\subseteq E,\\, (\\mathcal{N}_s(x) \\leq \\mathcal{N}_t(x)) \\Rightarrow \n\\mathrm{TangentCone}_\\mathbb{K}(s,x) \\subseteq \\mathrm{TangentCone}_\\mathbb{K}(t,x)$$$
Lean4
theorem tangentConeAt_mono_nhds (h : 𝓝[s] x ≤ 𝓝[t] x) : tangentConeAt 𝕜 s x ⊆ tangentConeAt 𝕜 t x :=
by
rintro y ⟨c, d, ds, ctop, clim⟩
refine ⟨c, d, ?_, ctop, clim⟩
suffices Tendsto (fun n => x + d n) atTop (𝓝[t] x) from tendsto_principal.1 (tendsto_inf.1 this).2
refine (tendsto_inf.2 ⟨?_, tendsto_principal.2 ds⟩).mono_right h
simpa only [add_zero] using tendsto_const_nhds.add (tangentConeAt.lim_zero atTop ctop clim)
