subset_generated

Mathlib.CategoryTheory.Groupoid.Subgroupoid

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

← MathLib Explorer

English

Arrows in X are contained in the generated subgroupoid's arrows.

Русский

Стрелы из X содержатся в стрелках порожденного подгруппоида.

LaTeX

$$$\forall c,d,\ X\,c\,d \subseteq (generated X).arrows\,c\,d$$$

Lean4

theorem subset_generated (c d : C) : X c d ⊆ (generated X).arrows c d :=
  by
  dsimp only [generated, sInf]
  simp only [subset_iInter₂_iff]
  exact fun S hS f fS => hS _ _ fS

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

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

Разделы

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

Аффилиация

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