uliftFunctorFullyFaithful

Mathlib.Topology.Category.TopCat.ULift

URI: https://scilib.ai/kg/mathlib#TopCat.uliftFunctorFullyFaithful

Lean4

/-- The `ULift` functor on categories of topological spaces is fully faithful. -/
def uliftFunctorFullyFaithful : uliftFunctor.{v, u}.FullyFaithful where
  preimage f := ofHom ⟨ULift.down ∘ f ∘ ULift.up, by continuity⟩

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

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

Разделы

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

Аффилиация

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