Growing sequence

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

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

predicate

$A_n\uparrow \hat A \equiv A\in \mathrm{GrowingSequence}(X)\ \land\ \lim_{n\to\infty}A_n=\hat A$