Theorems · Theorem · general topology

Metric.isBounded_iff_eventually

∀ {α : Type u} [inst : PseudoMetricSpace α] {s : Set α},
  Bornology.IsBounded s ↔ ∀ᶠ (C : ℝ) in Filter.atTop, ∀ ⦃x : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ s → dist x y ≤ C

Defined in

Mathlib.Topology.MetricSpace.Pseudo.Defs

Cited by

2 results in Mathlib

Foundations

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

Assumes

PseudoMetricSpace