Registry · Lemma VII.L29 tau-effective formalized

VII.L29 — F Lattice Completeness

The poset of j_dig-closed operator graphs F is a complete lattice; arbitrary intersections preserve j-closure.

Book VII Part 7 Ch. 89

Dependency Graph

Depends on (2)

VII.D71 VII.T35

Lean Formalization

Module: TauLib.BookVII.Ethics.CIProof

Symbol: Tau.BookVII.Ethics.CIProof.f_lattice_completeness