Fungrim entry: 6c22c8

Symbol: PrimePi —

\pi(x)

— Prime counting function

Domain	Codomain
$x \in \mathbb{R}$	$\pi(x) \in \mathbb{Z}_{\ge 0}$
$x \in \left\{\infty\right\}$	$\pi(x) \in \left\{\infty\right\}$

Table data:

\left(P, Q\right)

such that

\left(P\right) \;\implies\; \left(Q\right)

Definitions:

Fungrim symbol	Notation	Short description
`PrimePi`	$\pi(x)$	Prime counting function
`RR`	$\mathbb{R}$	Real numbers
`ZZGreaterEqual`	$\mathbb{Z}_{\ge n}$	Integers greater than or equal to n
`Infinity`	$\infty$	Positive infinity

Source code for this entry:

Entry(ID("6c22c8"),
    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

Prime numbers

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