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

A set where every point has a neighborhood entirely within the set. More...

Concept definition

template<typename S>
concept dedekind::topology::IsOpen =
dedekind::category::IsPredicate<S> &&
(dedekind::category::IsBoundaryObject<S> || HasDiscreteCarrier<S> ||
is_order_open_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::IsOpen
A set where every point has a neighborhood entirely within the set.
Definition neighborhood.cppm:191
dedekind::topology::is_order_open_v
constexpr bool is_order_open_v
Is S order-open by its strictness? false unless a specialisation below (or a carrier's own) says so.
Definition neighborhood.cppm:112

Detailed Description

A set where every point has a neighborhood entirely within the set.

A set where every point has a neighborhood entirely within the set — in the carrier's order topology.

Note
Arity: Updated to structuralist 1-arg IsSet.

Inferred, never tagged: ∅ and X (the boundary subobjects) are clopen in every topology; on a discrete carrier every subset is clopen (HasDiscreteCarrier); otherwise the shape's strictness decides (is_order_open_v).