From Encyclopedia of Mathematics
Revision as of 17:25, 7 February 2011 by (talk) (Importing text file)
(diff) ← Older revision | Latest revision (diff) | Newer revision → (diff)
Jump to: navigation, search

finitary spread

A spread (cf. Spread (in intuitionistic logic)) such that for any node of there exists only a finite number of natural numbers for which is a node of .

In the language of formal intuitionistic mathematical analysis, the function , which expresses the concept "the function a defines a fan" , is written as


where means "the function a defines a spread" .

Brouwer's fan theorem: If there exists a rule with the aid of which a certain object — say, a natural number — can be assigned to each element of a fan, then there exists a natural number such that for each element of the fan this object is defined by the first values of the element. Brouwer's theorem is used in proving many specifically intuitionistic facts such as the uniform continuity of every real function defined on a closed interval. In formal intuitionistic mathematical analysis Brouwer's fan theorem is usually proved with the aid of bar induction and Brouwer's continuity principle (cf. Intuitionism). In the language of this formal theory the fan theorem may be written down as follows:


[1] S.C. Kleene, R.E. Vesley, "The foundations of intuitionistic mathematics: especially in relation to recursive functions" , North-Holland (1965)


Formula (*) can be read as: An element of a fan is an infinite sequence all finite initial segments of which belong to .


[a1] A.S. Troelstra, "Choice sequences" , Clarendon Press (1977)
How to Cite This Entry:
Fan. Encyclopedia of Mathematics. URL:
This article was adapted from an original article by A.G. Dragalin (originator), which appeared in Encyclopedia of Mathematics - ISBN 1402006098. See original article