mem_closure_of_frequently_of_tendsto

English

If f: α → X tends to x along b and there exists a frequent x in b with f x ∈ s, then x ∈ closure(s).

Русский

Если f: α → X стремится к x по b и существует частая точка x в b с f x ∈ s, то x ∈ cl(s).

LaTeX

$$x ∈ \\overline{s}$$

Lean4

theorem mem_closure_of_frequently_of_tendsto {f : α → X} {b : Filter α} (h : ∃ᶠ x in b, f x ∈ s)
    (hf : Tendsto f b (𝓝 x)) : x ∈ closure s :=
  (hf.frequently h).mem_closure

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