neighborhood.cppm File Reference

The Rules of Continuity (Neighborhoods, Limits, and Cuts). More...

#include <concepts>
#include <functional>
#include <type_traits>
import dedekind.order;
import dedekind.sets;
import dedekind.category;

Include dependency graph for neighborhood.cppm:

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).
concept	dedekind::topology::IsConvexMagmoid
	Convex sets form a Magmoid under the intersection operation.

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::detail_order_reading::sides_are (const T &t, Side in)
	Whether every step of a decidable set term enters at the side in and leaves at the other: open enters just above a value, closed at it. An L-valued set is read through its α-cuts.
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 T, typename L>
constexpr bool	dedekind::topology::is_order_closed_v< Singleton< T, L > > = true
template<typename A, typename B>
constexpr bool	dedekind::topology::is_order_open_v< Meet< A, B > >
template<typename A, typename B>
constexpr bool	dedekind::topology::is_order_closed_v< Meet< A, B > >
template<typename A, typename B>
constexpr bool	dedekind::topology::is_order_open_v< Join< A, B > >
template<typename A, typename B>
constexpr bool	dedekind::topology::is_order_closed_v< Join< A, B > >
template<typename A>
constexpr bool	dedekind::topology::is_order_open_v< Not< A > > = is_order_closed_v<A>
template<typename A>
constexpr bool	dedekind::topology::is_order_closed_v< Not< A > > = is_order_open_v<A>
template<typename S>
constexpr bool	dedekind::topology::is_convex_v = false
template<typename T, typename L>
constexpr bool	dedekind::topology::is_convex_v< Interval< T, L > > = true
template<typename T, typename L>
constexpr bool	dedekind::topology::is_convex_v< Singleton< T, L > > = true
template<typename A, typename B>
constexpr bool	dedekind::topology::is_convex_v< Meet< A, B > >

Detailed Description

The Rules of Continuity (Neighborhoods, Limits, and Cuts).

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

@partition :topology @build_order 6 @dependency :algebra, :order

neighborhood__Topology

This partition establishes the qualitative "shape" of our species. It transforms discrete algebraic structures (like Q) into continuous spaces (like R) by defining the concepts of "closeness" and "convergence".

This module defines the formal boundaries of the continuum:

• IsOpen / IsClosed: The "Skin" and "Body" of a set.
• IsNeighborhood: The "Space Around" a point.
• IsSequence / HasLimit: The "Path" to a point (Convergence).
• IsDedekindComplete: The "Seamless" property (No gaps).

neighborhood__Structural_Synthesis

We synthesize the Order from (:order) and the Metric from (:algebra) to define the 'Dedekind Cut'. This is the ultimate "Promotion" in the library: moving from the Discrete (N, Z) to the Continuous (R).

@anchors C++ Concepts: std::floating_point (The Machine Approximation of R).

Wikipedia: Topology, Dedekind cut, Metric space, Limit of a sequence

Copyright

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

Note

"I am superior, sir, in many ways. But I would gladly give it up, to be Human." – Data, Star Trek: The Next Generation, "Encounter at Farpoint" (1987)

Variable Documentation

is_convex_v

template<typename S>

bool dedekind::topology::is_convex_v = false

inlineconstexprexport

neighborhood__Topology_2

is_convex_v< Meet< A, B > >

template<typename A, typename B>

bool dedekind::topology::is_convex_v< Meet< A, B > >

inlineconstexpr

Initial value:

=
    is_convex_v<A> && is_convex_v<B>

is_order_closed_v< Join< A, B > >

template<typename A, typename B>

bool dedekind::topology::is_order_closed_v< Join< A, B > >

inlineconstexpr

Initial value:

=
    is_order_closed_v<A> && is_order_closed_v<B>

is_order_closed_v< Meet< A, B > >

template<typename A, typename B>

bool dedekind::topology::is_order_closed_v< Meet< A, B > >

inlineconstexpr

Initial value:

=
    is_order_closed_v<A> && is_order_closed_v<B>

is_order_open_v

template<typename S>

bool dedekind::topology::is_order_open_v = false

inlineconstexprexport

Is S order-open by its strictness? false unless a specialisation below (or a carrier's own) says so.

neighborhood__Order_Reading

The order-topology reading of order's shapes, inferred from their strictness — the datum is order-theoretic (does the pivot belong: > vs ≥), the open / closed verdict is its topological consequence on a dense chain: a strict ray is open, a non-strict one closed, a point is closed, finite meets / joins preserve both, and complement swaps them. On a discrete carrier HasDiscreteCarrier makes everything clopen regardless. No shape carries a hand tag.

is_order_open_v< Join< A, B > >

template<typename A, typename B>

bool dedekind::topology::is_order_open_v< Join< A, B > >

inlineconstexpr

Initial value:

=
    is_order_open_v<A> && is_order_open_v<B>

is_order_open_v< Meet< A, B > >

template<typename A, typename B>

bool dedekind::topology::is_order_open_v< Meet< A, B > >

inlineconstexpr

Initial value:

=
    is_order_open_v<A> && is_order_open_v<B>