le_objs

Mathlib.CategoryTheory.Groupoid.Subgroupoid

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

English

If S ≤ T, then S.objs ⊆ T.objs (monotonicity of objects under inclusion).

Русский

Если S ≤ T, то S.objs ⊆ T.objs (монотонность множеств объектов).

LaTeX

$$S ≤ T → S.objs ⊆ T.objs$$

Lean4

theorem le_objs {S T : Subgroupoid C} (h : S ≤ T) : S.objs ⊆ T.objs := fun s ⟨γ, hγ⟩ => ⟨γ, @h ⟨s, s, γ⟩ hγ⟩

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

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

Разделы

Аффилиация

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