Abstract
Este trabajo busca: establecer una prueba del Teorema de Tychonoff, sin utilizar el axioma de elección, sobre la topología formal, la cual se fundamenta en la teoría de tipos de Martin Löf y estudiar los efectos que ocurren en la prueba del teorema, el cambio de la estructura de reticulo en los que se de nen los filtros, sistemas de vecindades y operador interior.