instIsEquivalenceUliftFunctorOfUnivLE

Mathlib.CategoryTheory.UnivLE

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

English

If UnivLE holds, then uliftFunctor is an equivalence.

Русский

Если существует UnivLE, то uliftFunctor является эксива-эквивалентностью.

LaTeX

$$$ [UnivLE] \\Rightarrow \\mathrm{uliftFunctor} \\text{ is an equivalence}$$$

Lean4

instance [UnivLE.{max u v, v}] : uliftFunctor.{u, v}.IsEquivalence where

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

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

Разделы

Аффилиация

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