English
Combining all replacements, one gets a consistent uniform structure that preserves the ambient normed structure.
Русский
Слияние всех замен даёт согласованную униформность, сохраняющую нормированную структуру.
LaTeX
$$$$\mathcal{U}_{ambient} = \mathcal{U}_{new}.$$$$
Lean4
/-- Produces a `NormedAddCommGroup E` instance from a `NormedSpace.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 [U : UniformSpace E] [B : Bornology E] (core : NormedSpace.Core 𝕜 E)
(HU : 𝓤[U] = 𝓤[PseudoEMetricSpace.toUniformSpace (self := PseudoEMetricSpace.ofSeminormedSpaceCore core.toCore)])
(HB :
∀ s : Set E,
@IsBounded _ B s ↔ @IsBounded _ (PseudoMetricSpace.ofSeminormedSpaceCore core.toCore).toBornology s) :
NormedAddCommGroup E :=
{ SeminormedAddCommGroup.ofCoreReplaceAll core.toCore HU HB with
eq_of_dist_eq_zero := by
intro x y h
rw [← sub_eq_zero, ← core.norm_eq_zero_iff]
exact h }
