Registry · Theorem I.T31 tau-effective formalized

I.T31 — Global Hartogs Extension

THE BOOK I CLIMAX. Global Hartogs Extension: any two tower-coherent functions agreeing at a reference depth agree at all depths below. Uses all four ingredients: spectral determination, CRT extension, tower coherence, and the Identity Theorem.

Book I Part 16 Ch. 62

Dependency Graph

Depends on (5)

I.T29 I.T30 I.T21 I.D46 I.L08

Depended on by (17)

I.C02 I.D68 I.T41 II.D49 II.D52 II.D72 II.L12 II.R01 II.R25 II.T34 II.T35 II.T37 II.T40 II.T44 II.T46 II.T47 III.P06

Lean Formalization

Module: TauLib.BookI.Holomorphy.GlobalHartogs

Symbol: Tau.Holomorphy.global_hartogs