## Infinite sequence

### Set

context | $X$ |

definiendum | $ A\in \mathrm{InfSequence}(X) $ |

postulate | $A: \mathbb N\to X$ |

### Discussion

Instead of $\langle n,A(n)\rangle$, we also write $A_n$ and denote the whole sequence by $(A_n)_{n\in\mathbb N}$ or just $(A_n)$.