hasGroupoid

Mathlib.Geometry.Manifold.Sheaf.Basic

URI: https://scilib.ai/kg/mathlib#TopCat.of.hasGroupoid

English

The carrier of TopCat.of M carries a HasGroupoid instance with respect to G.

Русский

Носитель TopCat.of M обладает структурой HasGroupoid по отношению к G.

LaTeX

$$HasGroupoid (TopCat.of M).carrier G$$

Lean4

instance hasGroupoid [HasGroupoid M G] : HasGroupoid (TopCat.of M) G :=
  (inferInstance : HasGroupoid M G)

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

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

Разделы

Аффилиация

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