Theorems · Theorem · general topology

UniformContinuousOn.comp

∀ {α : Type ua} {β : Type ub} {γ : Type uc} [inst : UniformSpace α] [inst_1 : UniformSpace β] [inst_2 : UniformSpace γ]
  {f : α → β} {s : Set α} {g : β → γ} {t : Set β},
  UniformContinuousOn g t → UniformContinuousOn f s → Set.MapsTo f s t → UniformContinuousOn (g ∘ f) s

Defined in

Mathlib.Topology.UniformSpace.Basic

Cited by

2 results in Mathlib

Foundations

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

Assumes

UniformSpaceUniformSpaceUniformSpace