Commit 2023-06-09 02:13 7a0fa5d5

View on Github →

feat: port CategoryTheory.Closed.Cartesian (#4829)

Estimated changes

Modified Mathlib.lean

Created Mathlib/CategoryTheory/Closed/Cartesian.lean

added def CategoryTheory.CartesianClosed.curry

added theorem CategoryTheory.CartesianClosed.curry_eq

added theorem CategoryTheory.CartesianClosed.curry_eq_iff

added theorem CategoryTheory.CartesianClosed.curry_id_eq_coev

added theorem CategoryTheory.CartesianClosed.curry_injective

added theorem CategoryTheory.CartesianClosed.curry_natural_left

added theorem CategoryTheory.CartesianClosed.curry_natural_right

added theorem CategoryTheory.CartesianClosed.curry_uncurry

added theorem CategoryTheory.CartesianClosed.eq_curry_iff

added theorem CategoryTheory.CartesianClosed.homEquiv_apply_eq

added theorem CategoryTheory.CartesianClosed.homEquiv_symm_apply_eq

added def CategoryTheory.CartesianClosed.uncurry

added theorem CategoryTheory.CartesianClosed.uncurry_curry

added theorem CategoryTheory.CartesianClosed.uncurry_eq

added theorem CategoryTheory.CartesianClosed.uncurry_id_eq_ev

added theorem CategoryTheory.CartesianClosed.uncurry_injective

added theorem CategoryTheory.CartesianClosed.uncurry_natural_left

added theorem CategoryTheory.CartesianClosed.uncurry_natural_right

added def CategoryTheory.binaryProductExponentiable

added def CategoryTheory.cartesianClosedOfEquiv

added theorem CategoryTheory.coev_app_comp_pre_app

added theorem CategoryTheory.exp.coev_ev

added def CategoryTheory.exp.delabPrefunctorObjExp

added theorem CategoryTheory.exp.ev_coev

added def CategoryTheory.expTerminalIsoSelf

added theorem CategoryTheory.initial_mono

added def CategoryTheory.internalHom

added def CategoryTheory.internalizeHom

added def CategoryTheory.mulZero

added def CategoryTheory.powZero

added def CategoryTheory.pre

added theorem CategoryTheory.pre_id

added theorem CategoryTheory.pre_map

added def CategoryTheory.prodCoprodDistrib

added theorem CategoryTheory.prod_map_pre_app_comp_ev

added theorem CategoryTheory.strict_initial

added def CategoryTheory.terminalExponentiable

added theorem CategoryTheory.uncurry_pre

added def CategoryTheory.zeroMul

Modified Mathlib/CategoryTheory/Yoneda.lean