Dedekind 0.0.0
A structuralist C++23 Module Library
Loading...
Searching...
No Matches
dedekind::topology::IsClosed Concept Referenceexport
module dedekind.topology

A set that contains all its limit points — in the carrier's order topology. Same three-leg inference as IsOpen. More...

Concept definition

template<typename S>
concept dedekind::topology::IsClosed =
dedekind::category::IsPredicate<S> &&
(dedekind::category::IsBoundaryObject<S> || HasDiscreteCarrier<S> ||
is_order_closed_v<std::remove_cvref_t<S>>)
dedekind::category::IsBoundaryObject
A type at a lattice / category bound: an initial object (⊥) or a terminal object (⊤).
Definition limit.cppm:249
dedekind::category::IsPredicate
The Predicate Morphism: the DSL's membership test, i.e. the characteristic arrow .
Definition topoi.cppm:104
dedekind::topology::HasDiscreteCarrier
The set's carrier is a discrete chain, so its order topology is the discrete topology — and there eve...
Definition neighborhood.cppm:91
dedekind::topology::IsClosed
A set that contains all its limit points — in the carrier's order topology. Same three-leg inference ...
Definition neighborhood.cppm:202
dedekind::topology::is_order_closed_v
constexpr bool is_order_closed_v
Is S order-closed by its strictness? Dual of is_order_open_v.
Definition neighborhood.cppm:116

Detailed Description

A set that contains all its limit points — in the carrier's order topology. Same three-leg inference as IsOpen.