Structural requirement for Dedekind completeness witnesses. More...

Concept definition

template<typename S>
concept dedekind::category::HasExtrema =  requires(S s) {
  
  { s.supremum() };
  
  { s.infimum() };
}

Detailed Description

Structural requirement for Dedekind completeness witnesses.

A type satisfies HasExtrema when it exposes both a supremum (least upper bound) and an infimum (greatest lower bound) operation. This is the structural prerequisite for IsDedekindComplete in the order partition.

Template Parameters

S	A carrier type (set or interval species).

See also: Dedekind (1872), Stetigkeit und irrationale Zahlen.; McLarty (1992), Elementary Categories, Elementary Toposes, ch. 4.