primeCounting_mono
plain-language theorem explainer
The prime counting function π is monotone: m ≤ n implies π(m) ≤ π(n). Number theorists cite this when bounding prime counts or applying order preservation in sieve estimates. The proof is a one-line wrapper that unfolds the local definition and invokes the standard Nat.monotone_primeCounting lemma.
Claim. Let π(n) denote the number of primes ≤ n. Then m ≤ n implies π(m) ≤ π(n).
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function μ. The prime counting function is defined by π(n) := Nat.primeCounting n, the cardinality of primes p with p ≤ n. This theorem records the order-preserving property of π under the natural ordering on ℕ.
proof idea
The proof is a one-line wrapper. It simplifies the goal using the definition of primeCounting and then applies Nat.monotone_primeCounting directly to the hypothesis h.
why it matters
This monotonicity statement supplies a basic order property of π inside the arithmetic-functions module. It supports later developments such as the Liouville-squarefree connection noted in the same file. No downstream uses are recorded, leaving open its precise role in larger Recognition Science arguments that may invoke prime distribution.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.