Registry · Definition I.D66 tau-effective formalized

I.D66 — Restriction Map

The restriction map: restrict a StageFun to inputs NOT in a given subset K. Returns 0 for deleted inputs. Agrees with original outside K.

Book I Part 16 Ch. 60

Dependency Graph

Depends on (1)

I.D47

Depended on by (1)

I.T29

Lean Formalization

Module: TauLib.BookI.Holomorphy.SpectralCoefficients

Symbol: Tau.Holomorphy.restriction