map_injective — Mathlib

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

Похожие утверждения