English
If f is injective, then the map that sends a nonunital star-subalgebra to its image is injective.
Русский
Если f инъективен, то отображение подпалгебр в их образы сохраняет различие: разные подалгебры дают разные образы.
LaTeX
$$If \(hf: \mathrm{Injective}(f)\), then the map \(S \mapsto \operatorname{map}(f,S)\) is injective, i.e. \(\operatorname{map}(f,S_1) = \operatorname{map}(f,S_2) \Rightarrow S_1 = S_2.\)$$
Lean4
theorem map_injective {f : F} (hf : Function.Injective f) :
Function.Injective (map f : NonUnitalStarSubalgebra R A → NonUnitalStarSubalgebra R B) := fun _S₁ _S₂ ih =>
ext <| Set.ext_iff.1 <| Set.image_injective.2 hf <| Set.ext <| SetLike.ext_iff.mp ih