Registry · Theorem IV.T18 tau-effective formalized

IV.T18 — Hilbert Space Properties

H_τ is complete, separable, infinite-dimensional — the three von Neumann axiom properties.

Book IV Part 3 Ch. 18

Dependency Graph

Depends on (2)

IV.D62 IV.D54

Depended on by (2)

IV.P19 IV.T19

Lean Formalization

Module: TauLib.BookIV.QuantumMechanics.HilbertSpace

Symbol: Tau.BookIV.QuantumMechanics.HilbertSpaceProperties