Registry · Lemma II.L06 established formalized

II.L06 — Gluing Lemma

Compatible tau-holomorphic sections on a cover by cylinder sub-domains glue uniquely to a global section, guaranteed by the ultrametric topology.

Book II Part 6 Ch. 36

Dependency Graph

Depends on (3)

Depended on by (1)

Lean Formalization

Module: TauLib.BookII.Hartogs.SheafCoherence

Symbol: gluing_lemma_check