primesBelow_card_eq_primeCounting'

English

The cardinality of primesBelow n equals primeCounting'(n): |n.primesBelow| = π'(n).

Русский

Число элементов множества primesBelow(n) равно π'(n).

LaTeX

$$$|n.\text{primesBelow}| = \pi'(n)$$$

Lean4

/-- The cardinality of the finset `primesBelow n` equals the counting function
`primeCounting'` at `n`. -/
theorem primesBelow_card_eq_primeCounting' (n : ℕ) : #n.primesBelow = primeCounting' n :=
  by
  simp only [primesBelow, primeCounting']
  exact (count_eq_card_filter_range Prime n).symm

Похожие утверждения