Registry · Lemma VII.L08 tau-effective formalized

VII.L08 — j-Closure Minimality

For structural invariant I with j-closed exhibitor, collection of I-exhibiting j-closed subobjects has minimum element unique up to isomorphism.

Book VII Part 1 Ch. 10

Dependency Graph

Depends on (2)

VII.D16 VII.D17

Depended on by (4)

VII.L12 VII.L24 VII.T08 VII.T35

Lean Formalization

Module: TauLib.BookVII.Meta.Archetypes

Symbol: Tau.BookVII.Meta.Archetypes.j_closure_minimality