Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-10-23 07:50 ee5518c2

View on Github →

fix(category_theory/adjunctions): fix deterministic timeouts (#1586)

Estimated changes

Modified src/category_theory/adjunction/basic.lean

Modified src/category_theory/adjunction/limits.lean

added def category_theory.adjunction.cocones_iso_component_hom

added def category_theory.adjunction.cocones_iso_component_inv

added def category_theory.adjunction.cones_iso_component_hom

added def category_theory.adjunction.cones_iso_component_inv

added def category_theory.adjunction.functoriality_counit'

added def category_theory.adjunction.functoriality_counit

added def category_theory.adjunction.functoriality_left_adjoint

added def category_theory.adjunction.functoriality_right_adjoint

added def category_theory.adjunction.functoriality_unit'

added def category_theory.adjunction.functoriality_unit

Modified src/category_theory/limits/cones.lean