Theorems · Theorem · general topology

PseudoMetricSpace.replaceBornology_eq

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

Defined in

Mathlib.Topology.MetricSpace.Pseudo.Defs

Cited by

0 results in Mathlib

Foundations

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

Assumes

PseudoMetricSpaceBornology