Commit 2023-02-22 03:15 f19681c5

View on Github →

feat: port CategoryTheory.LiftingProperties.Basic (#2325)

Estimated changes

Modified Mathlib.lean

Created Mathlib/CategoryTheory/LiftingProperties/Basic.lean

added theorem CategoryTheory.HasLiftingProperty.iff_of_arrow_iso_left

added theorem CategoryTheory.HasLiftingProperty.iff_of_arrow_iso_right

added theorem CategoryTheory.HasLiftingProperty.iff_op

added theorem CategoryTheory.HasLiftingProperty.iff_unop

added theorem CategoryTheory.HasLiftingProperty.of_arrow_iso_left

added theorem CategoryTheory.HasLiftingProperty.of_arrow_iso_right

added theorem CategoryTheory.HasLiftingProperty.op

added theorem CategoryTheory.HasLiftingProperty.unop