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

A monotone sequence. Bishop §2; together with IsBoundedSequence drives the monotone-convergence upgrade (LEM-gated, #719 Slice 5). More...

Concept definition

template<typename Seq>
concept dedekind::sequences::IsMonotoneSequence = IsSequence<Seq> && is_monotone_sequence_v<Seq>
dedekind::sequences::IsMonotoneSequence
A monotone sequence. Bishop §2; together with IsBoundedSequence drives the monotone-convergence upgra...
Definition convergence.cppm:338
dedekind::sequences::IsSequence
The fundamental mapping from a Domain Set to a Value Type.
Definition net.cppm:215
dedekind::sequences::is_monotone_sequence_v
constexpr bool is_monotone_sequence_v
Opt-in: Seq is monotone (s(n) ≤ s(n+1) for all n, or the reverse). Direction is the witness's concern...
Definition convergence.cppm:331

Detailed Description

A monotone sequence. Bishop §2; together with IsBoundedSequence drives the monotone-convergence upgrade (LEM-gated, #719 Slice 5).