English
Create a new metric space by replacing the bornology with a given bornology, preserving boundedness structure.
Русский
Создать новое метрическое пространство путём замены бороности на заданную, сохранив структуру ограниченности.
LaTeX
$$ReplaceBornology\;{α} [B: Bornology α] (m: MetricSpace α) (H: ∀ s, @IsBounded _ B s ↔ @IsBounded _ PseudoMetricSpace.toBornology s) : MetricSpace α$$
Lean4
/-- Build a new metric 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].
-/
abbrev replaceBornology {α} [B : Bornology α] (m : MetricSpace α)
(H : ∀ s, @IsBounded _ B s ↔ @IsBounded _ PseudoMetricSpace.toBornology s) : MetricSpace α :=
{ PseudoMetricSpace.replaceBornology _ H, m with toBornology := B }
