Registry · Lemma II.L13 established formalized

II.L13 — Stagewise Naturality

Stagewise Naturality

Book II Part 9 Ch. 49

Dependency Graph

Depends on (4)

II.T37 II.D36 II.T27 I.T18

Depended on by (4)

II.L14 II.T38 II.T39 II.T40

Lean Formalization

Module: TauLib.BookII.CentralTheorem.ExtensionsOmegaGerms

Symbol: Tau.BookII.CentralTheorem.stagewise_naturality_check