map_mono — Mathlib

English

If S1 is contained in S2, then the image under f of S1 is contained in the image under f of S2.

Русский

Если S1 содержится в S2, то образ f(S1) содержится в образ f(S2).

LaTeX

$$S_1 \le S_2 \Rightarrow \operatorname{map}(f,S_1) \le \operatorname{map}(f,S_2).$$

Lean4

theorem map_mono {S₁ S₂ : NonUnitalStarSubalgebra R A} {f : F} :
    S₁ ≤ S₂ → (map f S₁ : NonUnitalStarSubalgebra R B) ≤ map f S₂ :=
  Set.image_mono

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