HepLean Documentation

Mathlib.Data.Rat.Cardinal

Cardinality of ℚ #

This file proves that the Cardinality of ℚ is ℵ₀

source
theorem Cardinal.mkRat :
Cardinal.mk ℚ = Cardinal.aleph0