Commit 2023-08-06 01:45 79a62b9e

View on Github →

feat: transfer Functor.Final across natural isomorphisms (#6232)

Estimated changes

Modified Mathlib/CategoryTheory/Comma.lean

added def CategoryTheory.Comma.mapLeftEq

added def CategoryTheory.Comma.mapLeftIso

added def CategoryTheory.Comma.mapRightEq

added def CategoryTheory.Comma.mapRightIso

Modified Mathlib/CategoryTheory/Limits/Final.lean

added theorem CategoryTheory.Functor.final_of_natIso

added theorem CategoryTheory.Functor.initial_of_natIso

Modified Mathlib/CategoryTheory/StructuredArrow.lean

added def CategoryTheory.CostructuredArrow.mapIso

added def CategoryTheory.CostructuredArrow.mapNatIso

added def CategoryTheory.StructuredArrow.mapIso

added def CategoryTheory.StructuredArrow.mapNatIso