Registry · Definition I.D67 tau-effective formalized

I.D67 — Primorial Thinness

A subset K is primordially thin at stage k if it occupies fewer than k-1 of the first k CRT positions (leaving >= 2 free directions). The tau-analog of codimension >= 2. Empty set is globally thin.

Book I Part 16 Ch. 61

Dependency Graph

Depends on (1)

Depended on by (1)

Lean Formalization

Module: TauLib.BookI.Holomorphy.Thinness

Symbol: Tau.Holomorphy.PrimoriallyThin