map_objs_eq

Mathlib.CategoryTheory.Groupoid.Subgroupoid

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

English

d lies in im φ hφ .objs iff there exists c with φ.obj c = d.

Русский

d принадлежит im φ hφ .objs тогда и только тогда, когда существует c с φ.obj c = d.

LaTeX

$$$d \in (im φ hφ).objs \iff \exists c, φ.obj c = d$$$

Lean4

@[simp]
theorem map_objs_eq (hφ : Function.Injective φ.obj) : (map φ hφ S).objs = φ.obj '' S.objs := by ext x;
  convert mem_map_objs_iff S φ hφ x

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

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

Разделы

Аффилиация

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