mono_iff_injective — Mathlib

English

In the category of types, a morphism f: X → Y is mono if and only if f is injective.

Русский

В категории типов морфизм f: X → Y является моно, если и только если он инъективен.

LaTeX

$$$$ \text{Mono } f \;\iff\; \text{Injective } f. $$$$

Lean4

/-- A morphism in `Type` is a monomorphism if and only if it is injective. -/
@[stacks 003C]
theorem mono_iff_injective {X Y : Type u} (f : X ⟶ Y) : Mono f ↔ Function.Injective f :=
  by
  constructor
  · intro H x x' h
    rw [← homOfElement_eq_iff] at h ⊢
    exact (cancel_mono f).mp h
  · exact fun H => ⟨fun g g' h => H.comp_left h⟩

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