Theorems · Theorem · general topology

Filter.tendsto_iff_seq_tendsto

∀ {α : Type u_1} {β : Type u_2} {f : α → β} {k : Filter α} {l : Filter β} [k.IsCountablyGenerated],
  Filter.Tendsto f k l ↔ ∀ (x : ℕ → α), Filter.Tendsto x Filter.atTop k → Filter.Tendsto (f ∘ x) Filter.atTop l

An abstract version of continuity of sequentially continuous functions on metric spaces: if a filter k is countably generated then Tendsto f k l iff for every sequence u converging to k, f ∘ u tends to l.

Defined in

Mathlib.Order.Filter.AtTopBot.CountablyGenerated

Cited by

5 results in Mathlib

Foundations

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

Assumes

Filter.IsCountablyGenerated