mono_iff_injective — Mathlib

English

A morphism f is mono if and only if it is injective as a function on underlying sets.

Русский

Морфизм f моно тогда и только тогда, когда он инъективен как отображение между множествами.

LaTeX

$$$ \text{Mono } f \iff \text{Injective } (f.\text{hom}) $$$

Lean4

@[to_additive]
theorem mono_iff_injective : Mono f ↔ Function.Injective f :=
  Iff.trans (mono_iff_ker_eq_bot f) <| MonoidHom.ker_eq_bot_iff f.hom

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