Fungrim entry: 04427b

\pi\!\left(x\right) = \left|\left\{ p : p \in \mathbb{P} \,\mathbin{\operatorname{and}}\, p \le x \right\}\right|

Assumptions:

x \in \mathbb{R}

TeX:

\pi\!\left(x\right) = \left|\left\{ p : p \in \mathbb{P} \,\mathbin{\operatorname{and}}\, p \le x \right\}\right|

x \in \mathbb{R}

Definitions:

Fungrim symbol	Notation	Short description
`PrimePi`	$\pi\!\left(x\right)$	Prime counting function
`Cardinality`	$\left\|S\right\|$	Set cardinality
`SetBuilder`	$\left\{ f\!\left(x\right) : P\!\left(x\right) \right\}$	Set comprehension
`PP`	$\mathbb{P}$	Prime numbers
`RR`	$\mathbb{R}$	Real numbers

Source code for this entry:

Entry(ID("04427b"),
    Formula(Equal(PrimePi(x), Cardinality(SetBuilder(p, p, And(Element(p, PP), LessEqual(p, x)))))),
    Variables(x),
    Assumptions(Element(x, RR)))

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.

2019-06-18 07:49:59.356594 UTC