Theorems · Theorem · general topology

ZeroAtInftyContinuousMap.bounded

∀ {F : Type u_1} {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : PseudoMetricSpace β] [inst_2 : Zero β]
  [inst_3 : FunLike F α β] [ZeroAtInftyContinuousMapClass F α β] (f : F), ∃ C, ∀ (x y : α), dist (f x) (f y) ≤ C

Defined in

Mathlib.Topology.ContinuousMap.ZeroAtInfty

Cited by

1 results in Mathlib

Foundations

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

Assumes

TopologicalSpacePseudoMetricSpaceZeroFunLikeZeroAtInftyContinuousMapClass