map_mono

Mathlib.CategoryTheory.Groupoid.Subgroupoid

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Subgroupoid.map_mono

← MathLib Explorer

English

If S ≤ T then map φ hφ S ≤ map φ hφ T.

Русский

Если S подмножество T, то их образы через map образуют включение map S ≤ map T.

LaTeX

$$$S \le T \Rightarrow map\ φ hφ S \le map\ φ hφ T$$$

Lean4

theorem map_mono (hφ : Function.Injective φ.obj) (S T : Subgroupoid C) : S ≤ T → map φ hφ S ≤ map φ hφ T := fun h =>
  (galoisConnection_map_comap φ hφ).monotone_l h

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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