Infinite

Statistics

Metric	Count
Definitions	0
Theorems `exists_infinite_primes`, `not_bddAbove_setOf_prime`	2
Total	2

Name	Kind	Assumes	Proves	Validates	Depends On
`exists_infinite_primes` 📖	mathematical	—	`Prime`	—	`factorial_pos` `minFac_prime` `le_of_not_ge` `dvd_factorial` `minFac_pos` `minFac_dvd` `Prime.not_dvd_one`
`not_bddAbove_setOf_prime` 📖	mathematical	—	`BddAbove` `setOf` `Prime`	—	`not_bddAbove_iff` `exists_infinite_primes`

---