Веер

финитарный поток, - поток [img: http://localhost:8080/file/010305-13.jpg]. такой, что для всякого узла [img: http://localhost:8080/file/010305-14.jpg] из [img: http://localhost:8080/file/010305-15.jpg] существует лишь конечное число натуральных k, для к-рых [img: http://localhost:8080/file/010305-16.jpg] является узлом [img: http://localhost:8080/file/010305-17.jpg]. На языке формального интуиционистского математич. анализа формула [img: http://localhost:8080/file/010305-18.jpg], выражающая понятие "функция азадает В.", записывается в виде [img: http://localhost:8080/file/010305-19.jpg] где [img: http://localhost:8080/file/010305-20.jpg] означает "функция азадает поток". Теорема Брауэра о веере: если имеется правило, согласно к-рому каждому элементу В. сопоставлен нек-рый объект, напр, натуральное число, то найдется натуральное г такое, что для всякого элемента В. этот объект определяется уже первыми z значениями элемента. Теорема Брауэра используется в доказательстве многих специфически интуиционистских фактов, таких, как равномерная непрерывность всякой действительнозначной функции, заданной на отрезке. В формальном интуиционистском математич. анализе теорема Брауэра о В. выводится обычно с помощью бар-индукции и принципа непрерывности Брауэра (см. Интуиционизм). На языке этой формальной теории теорема о В. может быть записана следующим образом: [img: http://localhost:8080/file/010305-21.jpg]