Registry · Remark VII.R54 tau-effective not_applicable

VII.R54 — Book II j-Closure Consistency

Cross-book check: VII.D16 Lawvere-Tierney axioms match Book II j-closure formulation; LT1-LT3 consistent across both books.

Book VII Part 1 Ch. 10

Dependency Graph

Depends on (1)

Lean Formalization

Module:

Symbol: