> Of course you can include two or five or ten equivalent formulations (like textbooks sometimes do) but still, not everything under the sun.

Note that mathlib currently includes duplicates of many theorems; I believe deduplication is an active goal (if not one seeing much labor right now).