Registry · Theorem I.T40 tau-effective formalized

I.T40 — Presheaf Characterization

HolFun = Nat(F, F_j) ∩ D-Hol: a tau-holomorphic function is a natural transformation from the primorial presheaf to its split-complex extension that satisfies sector independence.

Book I Part 19 Ch. 74

Dependency Graph

Depends on (6)

I.D83 I.D46 I.D47 I.D53 I.P22 I.T18

Depended on by (5)

I.T41 II.D50 II.D53 II.R12 II.T36

Lean Formalization

Module: TauLib.BookI.Holomorphy.PresheafEssence

Symbol: presheaf_characterization