Registry · Lemma VII.L27 tau-effective formalized

VII.L27 — Sheaf Gluing Verification

Under τ-holomorphy, the sheaf condition can be verified on any single sufficiently fine τ-holomorphic cover.

Book VII Part 7 Ch. 77

Dependency Graph

Depends on (2)

VII.D66 VII.T31

Lean Formalization

Module: TauLib.BookVII.Ethics.CIProof

Symbol: Tau.BookVII.Ethics.CIProof.sheaf_gluing_verification