Documentation
Mathlib
.
Data
.
Rat
.
Cardinal
Search
Google site search
return to top
source
Imports
Init
Mathlib.Algebra.CharZero.Infinite
Mathlib.Algebra.Ring.Rat
Mathlib.Data.Rat.Encodable
Mathlib.SetTheory.Cardinal.Basic
Imported by
Cardinal
.
mkRat
Cardinality of ℚ
#
This file proves that the Cardinality of ℚ is ℵ₀
source
theorem
Cardinal
.
mkRat
:
Cardinal.mk
ℚ
=
Cardinal.aleph0