Registry · Lemma VII.L24 tau-effective formalized

VII.L24 — Lattice Closure

j-closed subobjects of a Grothendieck topos form a complete lattice; intersection of j-closed subobjects is j-closed.

Book VII Part 1 Ch. 10

Dependency Graph

Depends on (1)

VII.L08

Lean Formalization

Module: TauLib.BookVII.Meta.Archetypes

Symbol: Tau.BookVII.Meta.Archetypes.lattice_closure