cardinality of prime numbers

Stream: maths

[Bulhwi Cha]

import Mathlib.Data.Nat.PrimeFin
import Mathlib.SetTheory.Cardinal.Basic

namespace Nat.Primes

instance countable' : Countable Primes := ⟨⟨Subtype.val, coe_nat_injective⟩⟩

def toSet := { p | Prime p }

instance infinite' : Infinite Primes :=
  ⟨fun finp ↦
    have fins : toSet.Finite := @Set.toFinite ℕ toSet finp
    infinite_setOf_prime fins⟩

open scoped Cardinal

theorem cardinal_mk_eq_aleph0 : #Primes = ℵ₀ := Cardinal.mk_eq_aleph0 Primes

end Nat.Primes

I've just proved in Lean that the cardinality of the type of prime numbers is aleph-null. Do we want to include some part of the above code in Mathlib?

[Eric Wieser]

I think those all look fine except def toSet := { p | Prime p } which seems pretty useless

[Kyle Miller]

docs#Set.Infinite.to_subtype is how you're meant to go to docs#Infinite

You'd write instance : Infinite {p | Prime p} := Nat.infinite_setOf_prime.to_subtype (untested)

[Kyle Miller]

This instance seems reasonable to add to Mathlib/Data/Nat/PrimeFin.lean

[Bulhwi Cha]

Thanks, everyone. I'll soon make a PR to Mathlib. Edit: see #6238.

Fixed code

import Mathlib.Data.Nat.PrimeFin
import Mathlib.SetTheory.Cardinal.Basic

namespace Nat.Primes

instance countable' : Countable Primes := ⟨⟨coeNat.coe, coe_nat_injective⟩⟩

instance infinite' : Infinite Primes := infinite_setOf_prime.to_subtype

open scoped Cardinal

theorem cardinal_mk_eq_aleph0 : #Primes = ℵ₀ := Cardinal.mk_eq_aleph0 Primes

end Nat.Primes

[Yury G. Kudryashov]

Should we have a Denumerable instance for primes?