one_mem_posTangentConeAt_iff_frequently

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]

Похожие утверждения