mem_of_tendsto — Mathlib

English

If s is closed, and f: α → X tends to x along b, and f x ∈ s frequently, 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_tendsto {f : α → X} {b : Filter α} [NeBot b] (hs : IsClosed s) (hf : Tendsto f b (𝓝 x))
    (h : ∀ᶠ x in b, f x ∈ s) : x ∈ s :=
  hs.mem_of_frequently_of_tendsto h.frequently hf

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