mathlib3
d711d2a2 - feat(set_theory/ordinal): Small iff cardinality less than `cardinal.univ` (#12887)

Commit

3 years ago

feat(set_theory/ordinal): Small iff cardinality less than `cardinal.univ` (#12887) Characterizes when a type is small in terms of its cardinality

Author

awainverse

Parents