LemmaStatement: AI-adaptedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck passaudited 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.

Every join-irreducible element of a distributive lattice is join-prime

Statement

Let $L$ be a finite distributive lattice and let $j\in L$ be join-irreducible. If $j\le a\vee b$ , then $j\le a$ or $j\le b$ . Thus $j$ is join-prime.

Facts & Assumptions

Given: A finite distributive lattice $L$ , a join-irreducible $j\in L$ , and elements $a,b\in L$ with $j\le a\vee b$ .

[F1]

In a lattice, $x\le y$ exactly when $x\wedge y=x$ ; distributivity gives $x\wedge(y\vee z)=(x\wedge y)\vee(x\wedge z)$ (Lattices, distributive lattices, and order ideals).

[F2]

If $j=u\vee v$ and $j$ is join-irreducible, then $j=u$ or $j=v$ (Join-irreducible elements of a nonempty finite lattice).

Proof

technique · direct

1.1

Since $j\le a\vee b$ , one has $j=j\wedge(a\vee b)$ . Distributivity rewrites this as $j=(j\wedge a)\vee(j\wedge b)$ .

givenF1

2.1

Join-irreducibility applied to step 1.1 gives $j=j\wedge a$ or $j=j\wedge b$ . These equalities are respectively equivalent to $j\le a$ or $j\le b$ .

step 1.1F1F2

3.1

Hence every join-irreducible element of a distributive lattice is join-prime.

step 2.1∎

Depends on

Used by

Birkhoff representation theorem: every finite distributive lattice is isomorphic to the lattice of order ideals of its join-irreducible poset Theorem

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 3 results over 3 levels. An arrow runs from a result to what uses it, and this result sits at the bottom with a heavier outline. Click the chart to enlarge it.

Sources

MIT OpenCourseWare 18.212, Lecture 16: Distributive lattices (standard reference, not scraped)