eventually_mem_of_tendsto_nhdsWithin

English

If f tends to nhdsWithin a s, then f(i) ∈ s for all sufficiently large i.

Русский

Если f сходится к окрестностям внутри s, то для почти всех аргументов f(i) ∈ s.

LaTeX

$$$$ (\\\\mathrm{Tendsto}\, f \\\\ l \\\\ (\\\\nhdsWithin a s)) \\\\Rightarrow \\\\forall^{\\\\infty} i \in l, f(i) \\\\in s. $$$$

Lean4

theorem eventually_mem_of_tendsto_nhdsWithin {f : β → α} {a : α} {s : Set α} {l : Filter β} (h : Tendsto f l (𝓝[s] a)) :
    ∀ᶠ i in l, f i ∈ s :=
  by
  simp_rw [nhdsWithin_eq, tendsto_iInf, mem_setOf_eq, tendsto_principal, mem_inter_iff, eventually_and] at h
  exact (h univ ⟨mem_univ a, isOpen_univ⟩).2

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