Falling sequence

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$

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