injective_of_mono

Mathlib.CategoryTheory.Types.Basic

URI: https://scilib.ai/kg/mathlib#CategoryTheory.injective_of_mono

English

If f: X ⟶ Y is mono, then f is injective.

Русский

Если f: X ⟶ Y моно, то он инъективен.

LaTeX

$$$$ \text{Injective } f; \quad \text{from Mono } f. $$$$

Lean4

theorem injective_of_mono {X Y : Type u} (f : X ⟶ Y) [hf : Mono f] : Function.Injective f :=
  (mono_iff_injective f).1 hf

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru