UnivLE_iff_essSurj

Mathlib.CategoryTheory.UnivLE

URI: https://scilib.ai/kg/mathlib#UnivLE_iff_essSurj

← MathLib Explorer

English

UnivLE is equivalent to the ess-surjectivity of the ulift functor.

Русский

UnivLE эквивалентно условию ess-surjectivity для ulift-функторa.

LaTeX

$$$ \\mathrm{UnivLE}.\\text{iff } \\mathrm{uliftFunctor}.\\mathrm{EssSurj} $$$

Lean4

theorem UnivLE_iff_essSurj : UnivLE.{max u v, v} ↔ (uliftFunctor.{u, v} : Type v ⥤ Type max u v).EssSurj :=
  ⟨fun _ => inferInstance, fun w => UnivLE.ofEssSurj w⟩

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

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

Разделы

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

Аффилиация

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