dedekind::topology::HasDiscreteCarrier Concept Reference

The set's carrier is a discrete chain, so its order topology is the discrete topology — and there every subset is clopen. More...

Concept definition

template<typename S>
concept dedekind::topology::HasDiscreteCarrier = 
    dedekind::category::IsPredicate<S> &&
    (std::integral<dedekind::category::Dom<S>> ||
     dedekind::category::HasNNOStep<dedekind::category::Dom<S>>)

Detailed Description

The set's carrier is a discrete chain, so its order topology is the discrete topology — and there every subset is clopen.

Detected structurally from the domain: a carrier with an NNO step (category::HasNNOStep — successor / predecessor exist: the built-in std::integral types and the ℕ proxy Cardinality; the ℤ proxy SignedCardinality joins the moment it declares its step) is successor-isolated, so no subset has a limit point outside itself and every subset is both open and closed. The step IS the discreteness witness: Peano's axioms (an injective successor with induction) leave no element strictly between n and succ(n), so a carrier that overloads successor / predecessor asserts exactly that covering relation — the same kind of semantic contract as registering is_associative_v. A dense carrier (Rational, Cut) has no such step and must not declare one. This is the structural source of clopen-ness on discrete carriers (#905); a dense carrier (Rational, Cut) has no step, so its open / closed status falls to the boundary structure — the genuine open ⊋ clopen witness a discrete carrier cannot provide.

Note

This is also the bridge between two topologies that the library keeps apart on purpose. IsOpen / IsClosed / IsClopen below speak the carrier's order topology; sets::HasDecidableMembership speaks the decidability (Sierpiński) topology, in which "clopen = decidable" (Smyth / Rosolini / Escardó). On a dense carrier the two differ — an open ray on ℚ is decidable (exact rationals) yet not order-closed — so neither concept may be defined from the other. On a discrete carrier the order topology IS discrete, every subset is order-clopen, and the two readings coincide: that is this concept.