Registry · Corollary I.C02 tau-effective formalized

I.C02 — Stages from Limit

The interior is determined by the boundary: two tower-coherent functions with the same boundary data (agreement at a reference depth) have the same interior values at all coarser stages.

Book I Part 16 Ch. 63

Dependency Graph

Depends on (2)

Depended on by (1)

Lean Formalization

Module: TauLib.BookI.Holomorphy.BoundaryInterior

Symbol: Tau.Holomorphy.interior_from_boundary