eqToHom_mem

Mathlib.CategoryTheory.Groupoid.Subgroupoid

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

← MathLib Explorer

English

If c=d, then eqToHom of the equality is a member of S.arrows c c when S is wide.

Русский

Если c=d, то eqToHom(h) ∈ S.arrows c c, когда S широка.

LaTeX

$$Sw.IsWide → ∀ {c d}, (h : c = d) → eqToHom h ∈ S.arrows c d$$

Lean4

theorem eqToHom_mem {S : Subgroupoid C} (Sw : S.IsWide) {c d : C} (h : c = d) : eqToHom h ∈ S.arrows c d := by cases h;
  simp only [eqToHom_refl]; apply Sw.id_mem c

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

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

Разделы

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

Аффилиация

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