Registry · Proposition II.P07 established formalized

II.P07 — Bipolar Channel Independence

Bipolar Channel Independence

Book II Part 6 Ch. 30

Dependency Graph

Depends on (6)

I.D21 I.T10 I.T18 II.D33 II.D36 II.T26

Lean Formalization

Module: TauLib.BookII.Hartogs.BndLift

Symbol: Tau.BookII.Hartogs.bipolar_channel_independence