English
For a real line, the point 1 belongs to the positive tangent cone of a set s at a point a if and only if a lies in the closure of (Ioi(a) ∩ s), where Ioi(a) = (a, ∞).
Русский
На вещественной прямой число 1 принадлежит положительному касательному конусу множества s в точке a тогда и только тогда, когда a принадлежит замыканию (Ioi(a) ∩ s), где Ioi(a) = (a, ∞).
LaTeX
$$$1 \in \operatorname{posTangentConeAt}(s,a) \iff a \in \overline{((a,\infty) \cap s)}$$$
Lean4
theorem one_mem_posTangentConeAt_iff_mem_closure : 1 ∈ posTangentConeAt s a ↔ a ∈ closure (Ioi a ∩ s) :=
by
constructor
· rintro ⟨c, d, hs, hc, hcd⟩
have : Tendsto (a + d ·) atTop (𝓝 a) := by
simpa only [add_zero] using
tendsto_const_nhds.add (tangentConeAt.lim_zero _ (tendsto_abs_atTop_atTop.comp hc) hcd)
apply mem_closure_of_tendsto this
filter_upwards [hc.eventually_gt_atTop 0, hcd.eventually (lt_mem_nhds one_pos), hs] with n hcn hcdn hdn
simp_all
· intro h
apply mem_posTangentConeAt_of_frequently_mem
rw [mem_closure_iff_frequently, ← map_add_left_nhds_zero, frequently_map] at h
simpa [nhdsWithin, frequently_inf_principal] using h
