English
Combining uniformity and bornology replacements, one obtains a SeminormedAddCommGroup E with compatible core-induced structure.
Русский
Сочетая замены униформности и борологии, получаем SeminormedAddCommGroup E с совместимой структурой ядра.
LaTeX
$$$$\text{CoreReplaceAll}(E)=\text{core, with uniformity and bornology replacements}.$$$$
Lean4
/-- Produces a `SeminormedAddCommGroup 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 ofCoreReplaceAll {𝕜 : Type*} {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) :
SeminormedAddCommGroup E :=
{ PseudoMetricSpace.ofSeminormedSpaceCoreReplaceAll core HU HB with }
