Registry · Proposition II.P12 established formalized

II.P12 — Enrichment Iteration

Enrichment Iteration

Book II Part 8 Ch. 44

Dependency Graph

Depends on (5)

II.D53 II.D54 II.D55 II.D56 II.L07

Depended on by (2)

Lean Formalization

Module: TauLib.BookII.Enrichment.TwoCategories

Symbol: Tau.BookII.Enrichment.enrichment_iteration_check