mem_of_frequently_of_tendsto — Mathlib

English

Let s be closed. If f: α → X tends to x along b and f(x) eventually lies in s, then x ∈ s.

Русский

Пусть s замкнуто. Если f: α → X стремится к x по фильтру b, и значения f часто лежат в s, то x ∈ s.

LaTeX

$$IsClosed(s) ∧ Tendsto f b (𝓝 x) ∧ (∀ᶠ a in b, f a ∈ s) ⇒ x ∈ s$$

Lean4

theorem mem_of_frequently_of_tendsto {f : α → X} {b : Filter α} (hs : IsClosed s) (h : ∃ᶠ x in b, f x ∈ s)
    (hf : Tendsto f b (𝓝 x)) : x ∈ s :=
  (hf.frequently <| show ∃ᶠ x in b, (fun y => y ∈ s) (f x) from h).mem_of_closed hs

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