Commit 2024-09-24 06:31 d6fde790

View on Github →

feat(NumberTheory/PrimeCounting): surjective and tendsto (#17006)

Estimated changes

Modified Mathlib/Data/Nat/Nth.lean

added theorem Nat.surjective_count_of_infinite_setOf

Modified Mathlib/NumberTheory/PrimeCounting.lean

modified theorem Nat.add_two_le_nth_prime

added theorem Nat.primeCounting_sub_one

modified theorem Nat.primesBelow_card_eq_primeCounting'

added theorem Nat.surjective_primeCounting'

added theorem Nat.surjective_primeCounting

added theorem Nat.tendsto_primeCounting'

added theorem Nat.tensto_primeCounting