Double Sequences and Iterated Limits in Regular Space
First, we define in Mizar , the Cartesian product of two filters bases and the Cartesian product of two filters. After comparing the product of two Fréchet filters on ℕ (F1) with the Fréchet filter on ℕ × ℕ (F2), we compare limF₁ and limF₂ for all double sequences in a non empty topological space. Endou, Okazaki and Shidama formalized in  the “convergence in Pringsheim’s sense” for double sequence of real numbers. We show some basic correspondences between the p-convergence and the filter convergence in a topological space. Then we formalize that the double sequence [...] converges in “Pringsheim’s sense” but not in Frechet filter on ℕ × ℕ sense. In the next section, we generalize some definitions: “is convergent in the first coordinate”, “is convergent in the second coordinate”, “the lim in the first coordinate of”, “the lim in the second coordinate of” according to , in Hausdorff space. Finally, we generalize two theorems: (3) and (4) from  in the case of double sequences and we formalize the “iterated limit” theorem (“Double limit” , p. 81, par. 8.5 “Double limite”  (TG I,57)), all in regular space. We were inspired by the exercises (2.11.4), (2.17.5)  and the corrections B.10 .