Generator

lattice

A generator in the logic library, called 8 times across 3 essays. Below: what it draws at its defaults and at each mode an essay asks for, what it checks while drawing, and everywhere it is used.

lattice is one function. Everything below came out of it during this build, at parameters taken from the essays rather than invented for this page — so a figure here is the same figure a reader meets in an essay, and if the generator changes, this page changes with it.

At its defaults

The 8 subsets of a set of 3, ordered by inclusionA Hasse diagram of the subsets of a small set, with an edge wherever one subset is another plus one element.{a}{b}{a,b}{c}{a,c}{b,c}{a,b,c}0123the 8 subsets of a set of 3, joined when one is the other plus a single element8 against 3: there is no way to label the subsets by the elements, and that is the whole theorem

show: "cantor"

A map from 3 elements into the 8 subsets, and the subset it missesThe Hasse diagram of subsets with an arrow from each element to the subset it is sent to, and the diagonal subset highlighted.{a}{b}{a,b}{c}{a,c}{b,c}{a,b,c}abcDf sends a ↦ {a,b}, b ↦ {a,c}, c ↦ {b,c}D = {b} — the elements left out of their own target — and no arrow points at it

What it checks while it draws

Collected by running the family and recording what it asserted, not written here. The count is how many separate times the claim was put to the test while these drawings were made.

Where it is called

Changing this generator changes every figure on this list. That is what makes the list worth publishing rather than keeping in a check script.

The whole library · What the figures prove