Growing sequence

Set

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

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\uparrow \hat A \equiv A\in \mathrm{GrowingSequence}(X)\ \land\ \lim_{n\to\infty}A_n=\hat A$

Parents

Subset of

Infinite sequence