Countable intersection

Set

context $X$
context $A\in \mathrm{Sequence}(X)$
context $n\in \mathbb N\cup\{\infty\}$
definiendum $\bigcap_{j=1}^n A_j \equiv \bigcap A(\mathrm{range}(n))$

Ramifications

Parents

Refinement of

Arbitrary intersection

Sequence