not_tendsto_iff_exists_frequently_notMem

English

Not Tendsto f l1 l2 holds iff there exists a set s in l2 such that f(x) misses s frequently.

Русский

Не существует схода f по l1 к l2 тогда и только тогда, когда найдется множество s ∈ l2, для которого f(x) часто не принадлежит s.

LaTeX

$$$$ \neg \operatorname{Tendsto} f l_1 l_2 \iff \exists s \in l_2, \exists^\infty x \in l_1, f(x) \notin s $$$$

Lean4

theorem not_tendsto_iff_exists_frequently_notMem {f : α → β} {l₁ : Filter α} {l₂ : Filter β} :
    ¬Tendsto f l₁ l₂ ↔ ∃ s ∈ l₂, ∃ᶠ x in l₁, f x ∉ s := by
  simp only [tendsto_iff_forall_eventually_mem, not_forall, exists_prop, not_eventually]

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