ι_mono

Mathlib.Topology.Gluing

URI: https://scilib.ai/kg/mathlib#TopCat.GlueData.ι_mono

English

In the glue setup, ι_i are monomorphisms.

Русский

В конфигурации склейки ι_i являются монообразованиями.

LaTeX

$$$\forall i, \text{Mono}(\iota_i)$$$

Lean4

instance ι_mono (i : D.J) : Mono (𝖣.ι i) :=
  (TopCat.mono_iff_injective _).mpr (D.ι_injective _)

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

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

Разделы

Аффилиация

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