Registry · Theorem II.T26 established formalized

II.T26 — BndLift Existence

For every stage n and holomorphic datum, the boundary lift exists and is the unique extension to stage n+1 satisfying tower coherence and diagonal discipline.

Book II Part 6 Ch. 30

Dependency Graph

Depends on (8)

I.T18 I.D20 I.D21 I.D24 I.T10 II.D33 II.D35 II.D36

Depended on by (5)

II.D39 II.L12 II.P07 II.T29 II.T44

Lean Formalization

Module: TauLib.BookII.Hartogs.BndLift

Symbol: Tau.BookII.Hartogs.bndlift_existence_check