dedekind.topology Module Reference

Concepts
concept	dedekind::topology::HasDiscreteCarrier
	The set's carrier is a discrete chain, so its order topology is the discrete topology — and there every subset is clopen.
concept	dedekind::topology::IsOpen
	A set where every point has a neighborhood entirely within the set.
concept	dedekind::topology::IsClosed
	A set that contains all its limit points — in the carrier's order topology. Same three-leg inference as IsOpen.
concept	dedekind::topology::IsClopen
	A set that is BOTH open and closed — the topological face of decidability.
concept	dedekind::topology::IsNeighborhood
	A set that "surrounds" a point p.
concept	dedekind::topology::IsConvex
	A Set that satisfies the convexity theorem (no holes).

Functions
template<IsTotallyOrdered T, typename L>
constexpr bool	dedekind::topology::is_order_open (const Interval< T, L > &s)
	Whether an interval is order-open: every present side strict (an absent side is both open and closed). A value fact, as the sides are.
template<IsTotallyOrdered T, typename L>
constexpr bool	dedekind::topology::is_order_closed (const Interval< T, L > &s)
	Whether an interval is order-closed: every present side non-strict.
template<IsStepTerm T> requires std::same_as<typename T::logic_species, Boole>
constexpr bool	dedekind::topology::is_order_open (const T &t)
	Whether a set term of a chain is order-open: it enters each run just above a value and leaves it just below one, so no member sits on an edge.
template<IsStepTerm T> requires std::same_as<typename T::logic_species, Boole>
constexpr bool	dedekind::topology::is_order_closed (const T &t)
	Whether a set term is order-closed: it enters and leaves each run at a value, the dual of is_order_open.

Variables
template<typename S>
constexpr bool	dedekind::topology::is_order_open_v = false
	Is S order-open by its strictness? false unless a specialisation below (or a carrier's own) says so.
template<typename S>
constexpr bool	dedekind::topology::is_order_closed_v = false
	Is S order-closed by its strictness? Dual of is_order_open_v.
template<typename S>
constexpr bool	dedekind::topology::is_convex_v = false

Files
file	src/main/modules/dedekind/topology/topology.cppm
	Open-sets, neighbourhood filters, and continuity witnesses.
file	src/main/modules/dedekind/topology/neighborhood.cppm
	The Rules of Continuity (Neighborhoods, Limits, and Cuts).