Registry · Lemma II.L01 established formalized

II.L01 — Naturality Forces Cylinder Compatibility

Naturality Forces Cylinder Compatibility

Book II Part 2 Ch. 11

Dependency Graph

Depends on (3)

I.D47 II.D10 I.T18

Depended on by (1)

II.T06

Lean Formalization

Module: TauLib.BookII.Domains.HolImpliesCont

Symbol: cyl_compat_check