Commit 2023-11-24 13:15 244c4fda

View on Github →

feat(CategoryTheory): more constructors for ComposableArrows (#8475)

Estimated changes

Modified Mathlib/CategoryTheory/ComposableArrows.lean

added theorem CategoryTheory.ComposableArrows.ext_succ

added theorem CategoryTheory.ComposableArrows.ext₂

added theorem CategoryTheory.ComposableArrows.ext₃

added def CategoryTheory.ComposableArrows.homMkSucc

added theorem CategoryTheory.ComposableArrows.homMkSucc_app_succ

added theorem CategoryTheory.ComposableArrows.homMkSucc_app_zero

added def CategoryTheory.ComposableArrows.homMk₂

added theorem CategoryTheory.ComposableArrows.homMk₂_app_one

added theorem CategoryTheory.ComposableArrows.homMk₂_app_two

added theorem CategoryTheory.ComposableArrows.homMk₂_app_zero

added def CategoryTheory.ComposableArrows.homMk₃

added theorem CategoryTheory.ComposableArrows.homMk₃_app_one

added theorem CategoryTheory.ComposableArrows.homMk₃_app_three

added theorem CategoryTheory.ComposableArrows.homMk₃_app_two

added theorem CategoryTheory.ComposableArrows.homMk₃_app_zero

added theorem CategoryTheory.ComposableArrows.hom_ext_succ

added theorem CategoryTheory.ComposableArrows.hom_ext₂

added theorem CategoryTheory.ComposableArrows.hom_ext₃

added def CategoryTheory.ComposableArrows.isoMkSucc

added def CategoryTheory.ComposableArrows.isoMk₂

added def CategoryTheory.ComposableArrows.isoMk₃

added theorem CategoryTheory.ComposableArrows.mk₂_surjective

added theorem CategoryTheory.ComposableArrows.mk₃_surjective

added theorem CategoryTheory.ComposableArrows.naturality'

added theorem CategoryTheory.ComposableArrows.precomp_surjective