Basic

Statistics

Metric	Count
Definitions	0
Theorems `small_Pi`, `small_of_injective`, `small_of_injective_of_exists`, `small_of_surjective`, `small_prod`, `small_quot`, `small_quotient`, `small_set`, `small_subsingleton`, `small_subtype`, `small_sum`	11
Total	11

Name	Kind	Assumes	Proves	Validates	Depends On
`small_Pi` 📖	—	`Small`	—	—	`Equiv.symm_apply_apply` `Shrink.congr_simp`
`small_of_injective` 📖	mathematical	—	`Small`	—	`small_map` `small_subtype`
`small_of_injective_of_exists` 📖	mathematical	—	`Small`	—	`small_of_surjective` `Function.leftInverse_invFun` `small_subsingleton` `IsEmpty.instSubsingleton`
`small_of_surjective` 📖	mathematical	—	`Small`	—	`small_of_injective` `Function.injective_surjInv`
`small_prod` 📖	mathematical	—	`Small`	—	—
`small_quot` 📖	mathematical	—	`Small`	—	`small_of_surjective` `Quot.mk_surjective`
`small_quotient` 📖	mathematical	—	`Small`	—	`small_of_surjective` `Quotient.mk_surjective`
`small_set` 📖	mathematical	—	`Small` `Set`	—	—
`small_subsingleton` 📖	mathematical	—	`Small`	—	`isEmpty_or_nonempty` `small_map` `small_zero`
`small_subtype` 📖	mathematical	—	`Small`	—	`small_map` `small_self`
`small_sum` 📖	mathematical	—	`Small`	—	—

---