Double sequences are important extension of the ordinary notion of a sequence. In this article we formalized three types of limits of double sequences and the theory of these limits.