Theorems · Theorem · general topology

isClosed_iUnion_closure_singleton_of_not_tendsto

∀ {X : Type u_1} [inst : TopologicalSpace X] {x : ℕ → X} [SequentialSpace X],
  (∀ (l : X) (φ : ℕ → ℕ), StrictMono φ → ¬Filter.Tendsto (x ∘ φ) Filter.atTop (nhds l)) → IsClosed (⋃ i, closure {x i})

If x : ℕ → X has no convergent subsequence, then ⋃ i, closure {x i} is closed.

Defined in

Mathlib.Topology.Sequences

Cited by

1 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceSequentialSpace