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$ |