map_injective — Mathlib

English

If the underlying function f is injective, then the map on subalgebras is injective: map f S1 = map f S2 implies S1 = S2.

Русский

Если базовая функция f инъективна, то отображение подпалгебр по f инъективно: map f S1 = map f S2 значит S1 = S2.

LaTeX

$$$ \\text{If } \\text{Injective}(f) \\text{ then } \\forall S_1,S_2:\\ (\\mathrm{map}\,f\,S_1 = \\mathrm{map}\,f\,S_2) \\Rightarrow (S_1 = S_2). $$$

Lean4

theorem map_injective {f : F} (hf : Function.Injective f) :
    Function.Injective (map f : NonUnitalSubalgebra R A → NonUnitalSubalgebra R B) := fun _S₁ _S₂ ih =>
  ext <| Set.ext_iff.1 <| Set.image_injective.2 hf <| Set.ext <| SetLike.ext_iff.mp ih

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