Cardinality

Statistics

Metric	Count
Definitions	0
Theorems `mk_complex`, `mk_univ_complex`, `not_countable_complex`	3
Total	3

Name	Kind	Assumes	Proves	Validates	Depends On
`mk_complex` 📖	mathematical	—	`Complex` `continuum`	—	`mk_congr` `mk_prod` `lift_id` `mk_real` `continuum_mul_self`
`mk_univ_complex` 📖	mathematical	—	`Set.Elem` `Complex` `Set.univ` `continuum`	—	`mk_univ` `mk_complex`

Name	Kind	Assumes	Proves	Validates	Depends On
`not_countable_complex` 📖	mathematical	—	`Set.Countable` `Complex` `Set.univ`	—	`Cardinal.le_aleph0_iff_set_countable` `not_le` `Cardinal.mk_univ_complex` `Cardinal.cantor`

---