Registry · Lemma VII.L25 tau-effective formalized

VII.L25 — Minimality Witness

The archetype is the unique element satisfying all three conditions (A1)-(A3); any j-closed I-exhibiting subobject contains the archetype.

Book VII Part 1 Ch. 10

Dependency Graph

Depends on (1)

VII.T08

Lean Formalization

Module: TauLib.BookVII.Meta.Archetypes

Symbol: Tau.BookVII.Meta.Archetypes.minimality_witness