Registry · Theorem II.T32 established formalized

II.T32 — Sheaf Axioms

The holomorphic presheaf O_tau on the cylinder topology is a sheaf: it satisfies locality and gluing for compatible local sections.

Book II Part 6 Ch. 36

Dependency Graph

Depends on (4)

II.D47 II.L06 II.D10 I.T18

Depended on by (5)

II.D52 II.D72 II.R12 II.T35 II.T49

Lean Formalization

Module: TauLib.BookII.Hartogs.SheafCoherence

Symbol: sheaf_axioms_check