map_mono — Mathlib

English

If f: A →ₐ[R] B is injective, then the induced map on subalgebras map f is injective.

Русский

Если f: A →ₐ[R] B инъективен, то индуцированное отображение на подалгебры map f инъективно.

LaTeX

$$$\text{Injective}(f) \Rightarrow \text{Injective}(\mathrm{map}\,f)$$$

Lean4

theorem map_mono {S₁ S₂ : Subalgebra R A} {f : A →ₐ[R] B} : S₁ ≤ S₂ → S₁.map f ≤ S₂.map f :=
  Set.image_mono

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