English
For a set s and a ∈ ℝ, the membership 1 in posTangentConeAt(s,a) is equivalent to the existence of frequently points x in the right-hand neighborhood of a (nhds_{>a}) with x ∈ s.
Русский
Для множества s и точки a ∈ ℝ равенство 1 в posTangentConeAt(s,a) эквивалентно существованию часто встречающихся точек x рядом справа от a такие, что x ∈ s.
LaTeX
$$$1 \in \operatorname{posTangentConeAt}(s,a) \iff \exists^{\mathrm{frequently}} x \in \mathcal{N}_{>a},\ x \in s$$$
Lean4
theorem one_mem_posTangentConeAt_iff_frequently : 1 ∈ posTangentConeAt s a ↔ ∃ᶠ x in 𝓝[>] a, x ∈ s :=
by
rw [one_mem_posTangentConeAt_iff_mem_closure, mem_closure_iff_frequently, frequently_nhdsWithin_iff, inter_comm]
simp_rw [mem_inter_iff]