dedekind::sequences::IsSubsequence Concept Reference

Sub is a subsequence of Sup (same Codomain, strictly increasing index map). Feeds the Bolzano-Weierstrass row (#719 Slice 5: every bounded sequence has a convergent subsequence). More...

Concept definition

template<typename Sub, typename Sup>
concept dedekind::sequences::IsSubsequence = 
    IsSequence<Sub> && IsSequence<Sup> &&
    std::same_as<typename Sub::Codomain, typename Sup::Codomain> &&
    is_subsequence_v<Sub, Sup>

Detailed Description

Sub is a subsequence of Sup (same Codomain, strictly increasing index map). Feeds the Bolzano-Weierstrass row (#719 Slice 5: every bounded sequence has a convergent subsequence).