cardinality.cppm File Reference

Re-export of dedekind.sets:cardinality with numbers-level proofs. More...

import dedekind.order;
import dedekind.numbers:natural;
import dedekind.sets;

Include dependency graph for cardinality.cppm:

Namespaces
namespace	dedekind::numbers

Typedefs
using	dedekind::numbers::C1 = dedekind::sets::ExtensionalCardinal<>
using	dedekind::numbers::Z1 = dedekind::sets::SignedExtensionalCardinal<>
using	dedekind::numbers::SC = dedekind::sets::SignedCardinality
using	dedekind::numbers::Card = dedekind::sets::Cardinality

Detailed Description

Re-export of dedekind.sets:cardinality with numbers-level proofs.

@partition :cardinality

The extensional cardinality carrier ExtensionalCardinal<W> is defined in dedekind.sets:cardinality (below the numbers and algebra layers), making it available for use in polynomial ring assertions in algebra.

This partition re-exports the set-level cardinality types and adds the two assertions that require dedekind.order and dedekind.numbers:natural:

• IsTotallyOrdered<ExtensionalCardinal<>> (needs order)
• IsNatural<ExtensionalCardinal<>> (needs numbers:natural)

Copyright

2026 The Dedekind Authors Licensed under the Apache License, Version 2.0.

Note

"Das Wesen der Mathematik liegt in ihrer Freiheit." ("The essence of mathematics lies entirely in its freedom.") – Georg Cantor, Grundlagen einer allgemeinen Mannigfaltigkeitslehre (1883)