Commit 2022-11-24 03:21 2dac4fdf

View on Github →

feat(Data/ULift): port from mathlib (#703) Based on leanprover-community/mathlib3port@ec25b1a1c540bc430225653b11b16558e83406d3 and leanprover-community/mathlib@e50b8c261b0a000b806ec0e1356b41945eda61f7.

Estimated changes

added theorem PLift.down_bijective
added theorem PLift.down_surjective
added theorem PLift.up_bijective
added theorem PLift.up_inj
added theorem PLift.up_injective
added theorem PLift.up_surjective
added theorem PLift.«exists»
added theorem PLift.«forall»
added theorem ULift.down_bijective
added theorem ULift.down_surjective
added theorem ULift.up_bijective
added theorem ULift.up_inj
added theorem ULift.up_injective
added theorem ULift.up_surjective
added theorem ULift.«exists»
added theorem ULift.«forall»