English
The same equivalence 0 < ‖a‖ₑ ↔ a ≠ 1 holds, reinforcing the positivity of EN-norm away from identity.
Русский
Та же эквивалентность 0 < ‖a‖ₑ ↔ a ≠ 1 закрепляет положительность EN-нормы вне единицы.
LaTeX
$$$0 < \\|a\\|_\\varepsilon \\iff a \\neq 1$$$
Lean4
/-- A group homomorphism from a `Group` to a `SeminormedGroup` induces a `SeminormedGroup`
structure on the domain. -/
@[to_additive /-- A group homomorphism from an `AddGroup` to a
`SeminormedAddGroup` induces a `SeminormedAddGroup` structure on the domain. -/
]
abbrev induced [Group E] [SeminormedGroup F] [MonoidHomClass 𝓕 E F] (f : 𝓕) : SeminormedGroup E :=
{
PseudoMetricSpace.induced f toPseudoMetricSpace with
norm := fun x => ‖f x‖
dist_eq := fun x y => by simp only [map_div, ← dist_eq_norm_div]; rfl }
-- See note [reducible non-instances]
