Commit 2022-12-17 09:18 0b5dd3e1

View on Github →

feat port: Logic.Small.Basic (#1079) d012cd09a9b256d870751284dd6a29882b0be105

Estimated changes

added def Shrink
added theorem Small.mk'
added theorem not_small_type
added theorem small_congr
added theorem small_lift
added theorem small_map
added theorem small_of_injective
added theorem small_of_surjective
added theorem small_subset
added theorem small_type