mem_posTangentConeAt_of_frequently_mem

English

If a vector y is frequently along a direction such that x + t y ∈ s, then y ∈ posTangentConeAt s x.

Русский

Если вектор y часто встречается так, что x + t y ∈ s, то y принадлежит posTangentConeAt(s,x).

LaTeX

$$$\\text{Frequent}(t\\mapsto x+t y) \\Rightarrow y \\in posTangentConeAt(s,x)$$$

Lean4

theorem mem_posTangentConeAt_of_frequently_mem (h : ∃ᶠ t : ℝ in 𝓝[>] 0, x + t • y ∈ s) : y ∈ posTangentConeAt s x :=
  by
  obtain ⟨a, ha, has⟩ := Filter.exists_seq_forall_of_frequently h
  refine ⟨a⁻¹, (a · • y), Eventually.of_forall has, tendsto_inv_nhdsGT_zero.comp ha, ?_⟩
  refine tendsto_const_nhds.congr' ?_
  filter_upwards [(tendsto_nhdsWithin_iff.1 ha).2] with n (hn : 0 < a n)
  simp [ne_of_gt hn]

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