full_whiskeringLeft

Mathlib.CategoryTheory.Localization.Predicate

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Localization.full_whiskeringLeft

← MathLib Explorer

English

The whiskeringLeft functor is full.

Русский

Функтор whiskeringLeft полно.

LaTeX

$$$ full\\ ((\\text{Functor.whiskeringLeft})\\, L) $$$

Lean4

theorem full_whiskeringLeft (L : C ⥤ D) (W) [L.IsLocalization W] (E : Type*) [Category E] :
    ((whiskeringLeft C D E).obj L).Full :=
  inferInstanceAs (whiskeringLeftFunctor' L W E).Full

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

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

Разделы

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

Аффилиация

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