Registry · Proposition II.P10 established formalized

II.P10 — Functions as Tau-Objects

Functions as Tau-Objects

Book II Part 7 Ch. 40

Dependency Graph

Depends on (4)

II.D50 II.L07 II.T34 II.D49

Depended on by (1)

II.L14

Lean Formalization

Module: TauLib.BookII.Regularity.PreYoneda

Symbol: preyoneda_bipolar_check