Theorems · Theorem · general topology

BoundedContinuousFunction.tendsto_iff_tendstoUniformly

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

Defined in

Mathlib.Topology.ContinuousMap.Bounded.Basic

Cited by

2 results in Mathlib

Foundations

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

Assumes

TopologicalSpacePseudoMetricSpace