Theorems · Theorem · general topology

mem_closure_of_frequently_of_tendsto

∀ {X : Type u} [inst : TopologicalSpace X] {α : Type u_1} {x : X} {s : Set X} {f : α → X} {b : Filter α},
  (∃ᶠ (x : α) in b, f x ∈ s) → Filter.Tendsto f b (nhds x) → x ∈ closure s

Defined in

Mathlib.Topology.Neighborhoods

Cited by

4 results in Mathlib

Foundations

Depth 65 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

TopologicalSpace