Small

📁 Source: Mathlib/Data/Countable/Small.lean

Statistics

Metric	Count
Definitions	0
Theorems toSmall, of_not_small	2
Total	2

Countable

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
toSmall 📖	mathematical	—	Small	—	exists_injective_nat small_of_injective small_zero

Uncountable

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
of_not_small 📖	mathematical	Small	Uncountable	—	uncountable_iff_not_countable Countable.toSmall

---

← Back to Index