mem_objs_of_tgt

Mathlib.CategoryTheory.Groupoid.Subgroupoid

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

English

If f ∈ S.arrows c d, then d ∈ S.objs.

Русский

Если f ∈ S.arrows c d, тогда d ∈ S.objs.

LaTeX

$$$f \\in S.arrows\\ c d \\Rightarrow d \\in S.objs$$$

Lean4

theorem mem_objs_of_tgt {c d : C} {f : c ⟶ d} (h : f ∈ S.arrows c d) : d ∈ S.objs :=
  ⟨Groupoid.inv f ≫ f, S.mul (S.inv h) h⟩

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

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

Разделы

Аффилиация

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