Registry · Lemma VII.L23 tau-effective formalized

VII.L23 — LT Axiom Verification

Verifies j_τ satisfies all three Lawvere-Tierney axioms (LT1 truth-closed, LT2 idempotent, LT3 meet-commute).

Book VII Part 1 Ch. 10

Dependency Graph

Depends on (1)

VII.D16

Lean Formalization

Module: TauLib.BookVII.Meta.Archetypes

Symbol: Tau.BookVII.Meta.Archetypes.lt_axiom_verification