Alphabeta Math
DefinitionDefinition: AI-adaptedProof: Not applicableaudited 2026-07-31
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.

Intervals in a poset; locally finite, lower-finite and upper-finite posets

Definition

Let (P,≤) be a poset (Partial order and partially ordered set). For comparable elements x≤y, the closed interval from x to y is

[x,y]:={z∈P:x≤z≤y}.

The principal ideal below y and the principal filter above x are

P≤y:={z∈P:z≤y},P≥x:={z∈P:x≤z}.

bwxuvytr[x;y]P∙yn[x;y]P¸xn[x;y]

The poset P is

  • locally finite when [x,y] is finite for every x≤y;
  • lower-finite when P≤y is finite for every y∈P;
  • upper-finite when P≥x is finite for every x∈P.

Here finite has the meaning of Finite, countably infinite, countable, uncountable, and finite cardinalities are those of The cardinality ∣A∣ of a finite set. Every lower-finite poset is locally finite because [x,y]⊆P≤y, and every upper-finite poset is locally finite because [x,y]⊆P≥x; both conclusions use that a subset of a finite set is finite (A subset of a finite set is finite, with ∣B∣≤∣A∣, and equality holds if and only if B=A).

Remarks

Local finiteness controls sums over one interval [x,y]. It does not imply that a whole principal ideal or principal filter is finite. The one-sided hypotheses are therefore stated separately because global inversion sums range over those larger sets.

Depends on

Used by

Dependency tree · two levels

16 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