instFullOverTopOverForget

Mathlib.CategoryTheory.MorphismProperty.Comma

URI: https://scilib.ai/kg/mathlib#CategoryTheory.MorphismProperty.instFullOverTopOverForget

English

The forgetful functor from Over to T is full.

Русский

Функтор забывания из Over в T полный.

LaTeX

$$$\\text{Over.forget }P\\Top X\\text{ is full}$$$

Lean4

instance : (Over.forget P ⊤ X).Full :=
  inferInstanceAs <| (Comma.forget _ _ _ _ _).Full

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

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

Разделы

Аффилиация

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