Registry · Proposition I.P24 tau-effective formalized

I.P24 — HolFun Associativity

HolFun composition is associative: (f1 o f2) o f3 = f1 o (f2 o f3). Follows from function extensionality. Together with identity and composition closure, HolFun forms a monoid.

Book I Part 13 Ch. 51

Dependency Graph

Depends on (2)

I.T20 I.T03

Depended on by (2)

I.D51 I.T22

Lean Formalization

Module: TauLib.BookI.Holomorphy.DiagonalProtection

Symbol: Tau.Holomorphy.stagefun_comp_assoc