The full free-Abelian group theorem

This module applies the unconditional fusion construction to the generic topological results in Wallace.FullTopology. The resulting theorem has no hypotheses.

noncomputable def Wallace.continuumFullSeparationPackage : SeparationPackage TriangularPreprocess.ContinuumIndex

The fully constructed character package on the canonical free Abelian group of rank continuum.

Equations

• One or more equations did not get rendered due to their size.