Registry · Lemma VII.L18 tau-effective formalized

VII.L18 — Enrichment Monotonicity

E_n ⊆ E_m for n ≤ m; each enrichment layer contains all structure from previous layers.

Book VII Part 1 Ch. 7

Dependency Graph

Depends on (1)

VII.L03

Lean Formalization

Module: TauLib.BookVII.Meta.Registers

Symbol: Tau.BookVII.Meta.Registers.enrichment_monotone