CounterexampleConstruction: Literature-sourcedVerification: AI-adaptedprecheck passaudited 2026-08-21

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

Counting-measure tails decrease to the empty set while every term has infinite measure

Statement refuted

The finiteness hypothesis in continuity from above cannot be deleted: a decreasing sequence may have empty intersection while all its measures remain $+ \infty$ .

Facts & Assumptions

Given: Counting measure $#$ on $N$ and $E_{k} = {n \in N : k \leq n}$ .

[L1]

Counting measure gives every infinite set value $+ \infty$ (Counting measure on an arbitrary set) and is a measure (Counting measure is a measure).

[L2]

Continuity from above assumes that some member of the decreasing sequence has finite measure (Continuity from above when one set has finite measure).

[L3]

The natural order is defined through addition (Order on the natural numbers), natural addition is cancellative (Addition is cancellative), and each $n + 1$ is strictly greater than $n$ (Discreteness: $σ (n)$ is the immediate successor).

Counterexample

technique · direct

1.1givenL3

The sequence decreases because $k + 1 \leq n$ implies $k \leq n$ , and $E_{0} = N$ .

1.2givenL1L3

Every $E_{k}$ is infinite, since $n \mapsto k + n$ injects $N$ into $E_{k}$ , so $# (E_{k}) = + \infty$ .

1.3givenL3

The intersection is empty: a natural $n$ does not belong to $E_{n + 1}$ .

2.1step 1.2step 1.3L1L2∎

Hence $# (⋂_{k} E_{k}) = 0$ but $\inf_{k} # (E_{k}) = + \infty$ . The hypothesis of [L2] fails at every index, exactly as required.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

20 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

G. Folland, Real Analysis, 2nd ed., Theorem 1.8(d) (standard reference, not scraped)