typeToPartialFunIsoPartialFunToPointed

Mathlib.CategoryTheory.Category.PartialFun

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

Lean4

/-- Forgetting that maps are total and making them total again by adding a point is the same as just
adding a point. -/
@[simps!]
noncomputable def typeToPartialFunIsoPartialFunToPointed : typeToPartialFun ⋙ partialFunToPointed ≅ typeToPointed :=
  NatIso.ofComponents
    (fun _ =>
      { hom := ⟨id, rfl⟩
        inv := ⟨id, rfl⟩
        hom_inv_id := rfl
        inv_hom_id := rfl })
    fun f =>
    Pointed.Hom.ext <|
      funext fun a =>
        Option.recOn a rfl fun a => by
          convert Part.some_toOption _
          simpa using (Part.get_eq_iff_mem (by trivial)).mp rfl

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

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

Разделы

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

Аффилиация

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