English
Combining replacement of uniformity and bornology, one obtains a pseudo-metric space that agrees with the existing uniform and bornological structures.
Русский
Комбинируя замену униформности и борологии, получаем псевдометрическое пространство, согласующееся с существующими униформной и борологической структурами.
LaTeX
$$$$\\text{uniformity\_HB} : \\text{Eq}(\\text{uniformity},\\text{uniformity}) \\land \\text{IsBounded equivalence},$$$$
Lean4
/-- Produces a `PseudoEMetricSpace E` instance from a `SeminormedSpace.Core` on a type that
already has a preexisting uniform space structure and a preexisting bornology. This requires proofs
that the uniformity induced by the norm is equal to the preexisting uniformity, and likewise for
the bornology. See note [reducible non-instances]. -/
abbrev ofSeminormedSpaceCoreReplaceAll {𝕜 E : Type*} [NormedField 𝕜] [AddCommGroup E] [Norm E] [Module 𝕜 E]
[U : UniformSpace E] [B : Bornology E] (core : SeminormedSpace.Core 𝕜 E)
(HU : 𝓤[U] = 𝓤[PseudoEMetricSpace.toUniformSpace (self := PseudoEMetricSpace.ofSeminormedSpaceCore core)])
(HB : ∀ s : Set E, @IsBounded _ B s ↔ @IsBounded _ (PseudoMetricSpace.ofSeminormedSpaceCore core).toBornology s) :
PseudoMetricSpace E :=
.replaceBornology (.replaceUniformity (.ofSeminormedSpaceCore core) HU) HB
