Theorems · Theorem · general topology

ZeroAtInftyContinuousMap.tendsto_iff_tendstoUniformly

∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : PseudoMetricSpace β] [inst_2 : Zero β] {ι : Type u_2}
  {F : ι → ZeroAtInftyContinuousMap α β} {f : ZeroAtInftyContinuousMap α β} {l : Filter ι},
  Filter.Tendsto F l (nhds f) ↔ TendstoUniformly (fun i => ⇑(F i)) (⇑f) l

Convergence in the metric on C₀(α, β) is uniform convergence.

Defined in

Mathlib.Topology.ContinuousMap.ZeroAtInfty

Cited by

0 results in Mathlib

Foundations

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

Assumes

TopologicalSpacePseudoMetricSpaceZero