Registry · Theorem I.T06 tau-effective formalized

I.T06 — Global Hartogs

Boundary determines interior: interior points earned without coordinates via holomorphic continuation. Book I climax and canonical passage to Book II.

Book I Part 16 Ch. 62

Dependency Graph

Depends on (3)

I.D22 I.D18 I.X02

Lean Formalization

Module: TauLib.BookI.Holomorphy.GlobalHartogs

Symbol: Tau.Holomorphy.global_hartogs