English
Construct a new pseudometric space by changing its bornology to another Bornology B, provided the boundedness relation agrees with the original bornology, yielding the same cobounded sets up to isomorphism.
Русский
Построение нового псевдометрического пространства путём заменыBornology на другую Bornology B, если условия сохранения ограниченности выполняются, так что coboundedSets совпадают в смысле эквивалентности.
LaTeX
$$$\\text{Abbrev replaceBornology }(m:\\text{PseudoMetricSpace }\\alpha)(H: \\forall s, IsBounded_B(s) \\leftrightarrow IsBounded_{m.toBornology}(s)) \\Rightarrow \\text{new } m' \\text{ with } toBornology := B$$$
Lean4
/-- 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].
-/
abbrev replaceBornology {α} [B : Bornology α] (m : PseudoMetricSpace α)
(H : ∀ s, @IsBounded _ B s ↔ @IsBounded _ PseudoMetricSpace.toBornology s) : PseudoMetricSpace α :=
{ m with
toBornology := B
cobounded_sets :=
Set.ext <| compl_surjective.forall.2 fun s => (H s).trans <| by rw [isBounded_iff, mem_setOf_eq, compl_compl] }
