Boolean sublattices and prefix chains

Abstract

Finite Boolean sublattices are represented by subsets or by bitmasks.

Definition 1.1 (Nonempty sublattices).

$$\forall n\in \mathrm{Nat},\forall L\in \mathrm{Finset}\left(\mathrm{Finset}\left(\mathrm{Fin}\left(n\right)\right)\right),\mathrm{IsSublattice}\left(L\right)\iff \left(\mathrm{Nonempty}\left(L\right)\wedge \left(\forall A\in \mathrm{Finset}\left(\mathrm{Fin}\left(n\right)\right),A\in L\Rightarrow \left(\forall B\in \mathrm{Finset}\left(\mathrm{Fin}\left(n\right)\right),B\in L\Rightarrow \left(\mathrm{union}\left(A,B\right)\in L\wedge \mathrm{inter}\left(A,B\right)\in L\right)\right)\right)\right)$$

Formalization. D5/S3/Combinatorics/ErdosUlam/SublatticeDefs.IsSublattice (✓ std3).

Source. Repository-derived.

Commentary.

A sublattice is a nonempty finite family closed under union and intersection.

Definition 1.2 (Constant colour).

$$\forall n\in \mathrm{Nat},\forall chi\in \mathrm{Finset}\left(\mathrm{Fin}\left(n\right)\right)\to \mathrm{Bool},\forall L\in \mathrm{Finset}\left(\mathrm{Finset}\left(\mathrm{Fin}\left(n\right)\right)\right),\mathrm{Monochromatic}\left(chi,L\right)\iff \left(\exists b\in \mathrm{Bool},\forall A\in \mathrm{Finset}\left(\mathrm{Fin}\left(n\right)\right),A\in L\Rightarrow \mathrm{chi}\left(A\right)=b\right)$$

Formalization. D5/S3/Combinatorics/ErdosUlam/SublatticeDefs.Monochromatic (✓ std3).

Source. Repository-derived.

Commentary.

All members of a monochromatic family have one common Boolean colour.

Theorem 1.3 (Cardinality of a prefix).

$$\forall n\in \mathrm{Nat},\forall r\in \mathrm{Nat},r\le n\Rightarrow \mathrm{card}\left(\mathrm{initialSegment}\left(n,r\right)\right)=r$$

Proof. Machine-checked in Lean as D5/S3/Combinatorics/ErdosUlam/SublatticeDefs.prefix_card (✓ std3). ∎

Source. Repository-derived.

Commentary.

The prefix of rank r consists of the first r elements when r is at most n. Prefixes are nested by rank. Bitmask decoding sends bitwise union and intersection to the corresponding subset operations.

References

• Truth anchor: D5/S3/Combinatorics/ErdosUlam/SublatticeDefs.IsSublattice
• Truth anchor: D5/S3/Combinatorics/ErdosUlam/SublatticeDefs.Monochromatic
• Truth anchor: D5/S3/Combinatorics/ErdosUlam/SublatticeDefs.prefix_card