Theorems · Definition · general topology

PseudoMetricSpace.replaceBornology

{α : Type u_3} →
  [B : Bornology α] →
    (m : PseudoMetricSpace α) → (∀ (s : Set α), Bornology.IsBounded s ↔ Bornology.IsBounded s) → PseudoMetricSpace α

Build a new pseudometric space from an old one where the bundled bornology structure is provably (but typically non-definitionaly) equal to some given bornology structure. See Note [forgetful inheritance]. See Note [reducible non-instances].

Defined in

Mathlib.Topology.MetricSpace.Pseudo.Defs

Cited by

1 results in Mathlib

Foundations

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

Assumes

Bornology