Commit 2023-02-15 04:55 f52a0950

View on Github →

feat port/CategoryTheory.Pi.Basic (#2230)

Estimated changes

Modified Mathlib.lean

Created Mathlib/CategoryTheory/Pi/Basic.lean

added theorem CategoryTheory.Functor.eqToHom_proj

added def CategoryTheory.Functor.pi'

added theorem CategoryTheory.Functor.pi'_eval

added def CategoryTheory.Functor.pi

added theorem CategoryTheory.Functor.pi_ext

added def CategoryTheory.NatTrans.pi

added def CategoryTheory.Pi.comap

added def CategoryTheory.Pi.comapComp

added def CategoryTheory.Pi.comapEvalIsoEval

added def CategoryTheory.Pi.comapId

added theorem CategoryTheory.Pi.comp_apply

added def CategoryTheory.Pi.eval

added theorem CategoryTheory.Pi.id_apply

added def CategoryTheory.Pi.isoApp

added theorem CategoryTheory.Pi.isoApp_refl

added theorem CategoryTheory.Pi.isoApp_symm

added theorem CategoryTheory.Pi.isoApp_trans

added def CategoryTheory.Pi.sum