Alphabeta MathDefinitionDefinition: Literature-sourcedProof: Not applicablejudge pass (deepseek-v4-pro + claude-sonnet-5)audited 2026-08-17
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.
Limit superior and limit inferior of a sequence of sets
Definition
For a sequence of subsets of a set , define
The sequence begins at index . If the two sets are equal, their common value is called the limit of the sequence of sets.
Used by
- First-return times and induced transformations Definition
- Limsup and the infinitely often event Definition
- Borel-Cantelli for the shrinking intervals (0,2⁻ᵏ) under a dyadic atomic measure Example
- Set liminf means eventual membership, set limsup means repeated membership, and liminf is contained in limsup Proposition
- Sigma-algebras are closed under countable intersections, differences, symmetric differences, and set limits Theorem
- The first Borel-Cantelli lemma for measures Theorem
- The limsup of the measures is at most the measure of the set limsup under a finite-union bound Theorem
- The measure of a set liminf is at most the liminf of the measures Theorem
Dependency tree · 0 levels
Nothing. This result depends on no other item in the library.
Sources
- R. F. Bass, Real Analysis for Graduate Students, version 5.0, Exercise 2.9 (standard reference, not scraped)