Dedekind completion

ID: dedekind-completion

The completion of a total order by its nonprincipal proper cuts, supplying least upper bounds. For a dense order it contains the original order densely, and preserves the interval countable chain condition and separability or nonseparability.

New to topics? Read the docs here!