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

A Cauchy sequence whose limit can be witnessed via limit(s). More...

Concept definition

template<typename Seq>
concept dedekind::sequences::IsConvergentSequence = IsCauchySequence<Seq> && requires(Seq s) {
{ limit(s) } -> std::same_as<typename Seq::Codomain>;
}
dedekind::sequences::IsCauchySequence
A Seq is a Cauchy sequence: its tail is eventually arbitrarily small under the metric on the carrier.
Definition convergence.cppm:90
dedekind::sequences::IsConvergentSequence
A Cauchy sequence whose limit can be witnessed via limit(s).
Definition convergence.cppm:111
dedekind::sequences::limit
constexpr T limit(const Path< T > &s)
The Archimedean Limit (lim n->∞ s_n).
Definition limits.cppm:66

Detailed Description

A Cauchy sequence whose limit can be witnessed via limit(s).

Strict refinement of IsCauchySequence by the existence of a limit(s) witness. Extracting limit(s) from a Cauchy sequence is the LEM-flavoured collapse step (Specker's recursive counterexample under ConstructiveLogic; classical under Boole). The carrier-axis cardinality cut determines whether the collapse fires honestly — see #719 Slice 5.

Anchor: Bishop §2.18. Form-chain row 6 of #719.