Falling sequence

Set

context $X$
definiendum $A\in \mathrm{FallingSequence}(X) $
postulate $A\in \mathrm{InfSequence}(X) $
$n\in \mathbb N$
postulate $A_{n+1}\subseteq A_n $

Discussion

Ramifications

For falling sequences we have: $\lim_{n\to\infty}A_n=\bigcap_{n=1}^\infty A_n$.

For growing sequences we have: $\lim_{n\to\infty}A_n=\bigcup_{n=1}^\infty A_n$.

Predicates

predicate $A_n\downarrow \hat A \equiv A\in \mathrm{FallingSequence}(X)\ \land\ \lim_{n\to\infty}A_n=\hat A$

Parents

Subset of

Infinite sequence