Theorems · Theorem · general topology

Metric.isBounded_image_iff

∀ {α : Type u} {β : Type v} [inst : PseudoMetricSpace α] {f : β → α} {s : Set β},
  Bornology.IsBounded (f '' s) ↔ ∃ C, ∀ x ∈ s, ∀ y ∈ s, dist (f x) (f y) ≤ C

Defined in

Mathlib.Topology.MetricSpace.Bounded

Cited by

1 results in Mathlib

Foundations

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

Assumes

PseudoMetricSpace