Theorems · Theorem · general topology

UniformContinuousOn.tendstoUniformly

∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : UniformSpace β] {x : α} [inst_1 : UniformSpace α]
  [inst_2 : UniformSpace γ] {U : Set α},
  U ∈ nhds x → ∀ {F : α → β → γ}, UniformContinuousOn (↿F) (U ×ˢ Set.univ) → TendstoUniformly F (F x) (nhds x)

Defined in

Mathlib.Topology.UniformSpace.UniformConvergence

Cited by

3 results in Mathlib

Foundations

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

Assumes

UniformSpaceUniformSpaceUniformSpace