Fungrim home page

Fungrim entry: 6c22c8

Symbol: PrimePi π(x)\pi(x) Prime counting function
Domain Codomain
xRx \in \mathbb{R} π(x)Z0\pi(x) \in \mathbb{Z}_{\ge 0}
x{}x \in \left\{\infty\right\} π(x){}\pi(x) \in \left\{\infty\right\}
Table data: (P,Q)\left(P, Q\right) such that (P)        (Q)\left(P\right) \;\implies\; \left(Q\right)
Fungrim symbol Notation Short description
PrimePiπ(x)\pi(x) Prime counting function
RRR\mathbb{R} Real numbers
ZZGreaterEqualZn\mathbb{Z}_{\ge n} Integers greater than or equal to n
Infinity\infty Positive infinity
Source code for this entry:
    SymbolDefinition(PrimePi, PrimePi(x), "Prime counting function"),
    Table(TableRelation(Tuple(P, Q), Implies(P, Q)), TableHeadings(Description("Domain"), Description("Codomain")), List(Tuple(Element(x, RR), Element(PrimePi(x), ZZGreaterEqual(0))), Tuple(Element(x, Set(Infinity)), Element(PrimePi(x), Set(Infinity))))))

Topics using this entry

Copyright (C) Fredrik Johansson and contributors. Fungrim is provided under the MIT license. The source code is on GitHub.

2021-03-15 19:12:00.328586 UTC