Mathlib Changelog
v4
Changelog
About
Github
Commit
2022-12-17 09:18
0b5dd3e1
View on Github →
feat port: Logic.Small.Basic (
#1079
) d012cd09a9b256d870751284dd6a29882b0be105
Estimated changes
Modified
Mathlib.lean
Created
Mathlib/Logic/Small/Basic.lean
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