English
If the continuousAt inner function is given and the unit ball is von Neumann bounded, the normed and topological structures coincide.
Русский
При условии непрерывности функции по внутреннему произведению и ограниченности единичной сферы по Вон Ньону, структуры нормированного пространства и топологии совпадают.
LaTeX
$$Eq of topologies: tF = (NormedAddCommGroup).toUniformSpace.toTopologicalSpace$$
Lean4
/-- Normed space structure constructed from an `InnerProductSpace.Core` structure, adjusting the
topology to make sure it is defeq to an already existing topology. -/
@[reducible]
def toNormedAddCommGroupOfTopology [tF : TopologicalSpace F] [IsTopologicalAddGroup F] [ContinuousConstSMul 𝕜 F]
(h : ContinuousAt (fun (v : F) ↦ cd.inner v v) 0) (h' : IsVonNBounded 𝕜 {v : F | re (cd.inner v v) < 1}) :
NormedAddCommGroup F :=
NormedAddCommGroup.ofCoreReplaceTopology cd.toNormedSpaceCore (cd.topology_eq h h')
