subtype_val_mono

Mathlib.CategoryTheory.Subobject.Types

URI: https://scilib.ai/kg/mathlib#subtype_val_mono

English

The inclusion of a subset s into α given by the subtype val map is a monomorphism.

Русский

Включение подмножества s в α по отображению Subtype.val является моно.

LaTeX

$$$\text{Mono}(\iota_s: s \hookrightarrow \alpha)$, где iota_s = (Subtype.val).$$

Lean4

theorem subtype_val_mono {α : Type u} (s : Set α) : Mono (↾(Subtype.val : s → α)) :=
  (mono_iff_injective _).mpr Subtype.val_injective

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

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

Разделы

Аффилиация

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