English
The induced NormedGroup structure is uniquely determined by the norms and distances pulled back along f; equality statements express that the induced norm and distance agree with the pulled-back data.
Русский
Структура Induced NormedGroup однозначно задаётся сходами норм и расстояний, вытянутых через f; равенства выражают соответствие норм и расстояний индукцированной структуры и вытянутых данных.
LaTeX
$$$\\text{NormedGroup.induced } E F f h = \\text{pullback along } f\\; (\\|\\cdot\\|_F, d_F)$$$
Lean4
/-- An injective group homomorphism from a `Group` to a `NormedGroup` induces a `NormedGroup`
structure on the domain. -/
@[to_additive /-- An injective group homomorphism from an `AddGroup` to a
`NormedAddGroup` induces a `NormedAddGroup` structure on the domain. -/
]
abbrev induced [Group E] [NormedGroup F] [MonoidHomClass 𝓕 E F] (f : 𝓕) (h : Injective f) : NormedGroup E :=
{ SeminormedGroup.induced E F f, MetricSpace.induced f h _ with }
-- See note [reducible non-instances].
