Theorems · Theorem · general topology

IsClosed.mem_of_tendsto

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

Defined in

Mathlib.Topology.Neighborhoods

Cited by

32 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceFilter.NeBot