instHasForget₂TopCat

Mathlib.CategoryTheory.Action.Continuous

URI: https://scilib.ai/kg/mathlib#Action.instHasForget₂TopCat

English

There is a forgetful functor from Action V G to TopCat in the Action.Continuous framework.

Русский

Существуют забывающие функторы из Action V G в TopCat в рамках Action.Continuous.

LaTeX

$$$\text{HasForget₂ (Action V G) TopCat}$$$

Lean4

instance : HasForget₂ (Action V G) TopCat :=
  HasForget₂.trans (Action V G) V TopCat

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

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

Разделы

Аффилиация

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