map_injective_of_injective — Mathlib

English

If f is injective, then map f is injective on Subsemigroups: distinct S map to distinct images.

Русский

Если f инъективно, то отображение образа на подполугруппах слабо инъективно: разные подполугруппы имеют разные образы.

LaTeX

$$Function.Injective (map f)$$

Lean4

@[to_additive]
theorem map_injective_of_injective : Function.Injective (map f) :=
  (gciMapComap hf).l_injective

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