Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
Change 1: Original page describes the fan theorem as requiring the bar to be decidable, claims that the “classical” fan theorem contradicts Brouwer’s continuity principle. The latter claim is not true; I corrected the error. I have stated the result as two separate theorems: the decidable fan theorem, about decidable bars, and the fan theorem, about bars in general.
Change 2: Slightly more information is provided about the relationship between the Fan Theorem and Bar Induction. Eventually, we should make a page about the latter.
Change 3: the section on equivalents to the fan theorem has been fixed somewhat. The section originally asserted that all of the statements provided were equivalent to the decidable fan theorem; in fact, some are equivalent to the decidable fan theorem and some to the full fan theorem.
Change 1: Original page describes the fan theorem as requiring the bar to be decidable, claims that the “classical” fan theorem contradicts Brouwer’s continuity principle. The latter claim is not true; I corrected the error. I have stated the result as two separate theorems: the decidable fan theorem, about decidable bars, and the fan theorem, about bars in general.
Change 2: Slightly more information is provided about the relationship between the Fan Theorem and Bar Induction. Eventually, we should make a page about the latter.
Change 3: the section on equivalents to the fan theorem has been fixed somewhat. The section originally asserted that all of the statements provided were equivalent to the decidable fan theorem; in fact, some are equivalent to the decidable fan theorem and some to the full fan theorem.
Change 1: Original page describes the fan theorem as requiring the bar to be decidable, claims that the “classical” fan theorem contradicts Brouwer’s continuity principle. The latter claim is not true; I corrected the error. I have stated the result as two separate theorems: the decidable fan theorem, about decidable bars, and the fan theorem, about bars in general.
Change 2: Slightly more information is provided about the relationship between the Fan Theorem and Bar Induction. Eventually, we should make a page about the latter.
Change 3: the section on equivalents to the fan theorem has been fixed somewhat. The section originally asserted that all of the statements provided were equivalent to the decidable fan theorem; in fact, some are equivalent to the decidable fan theorem and some to the full fan theorem.
Change 1: Original page describes the fan theorem as requiring the bar to be decidable, claims that the “classical” fan theorem contradicts Brouwer’s continuity principle. The latter claim is not true; I corrected the error. I have stated the result as two separate theorems: the decidable fan theorem, about decidable bars, and the fan theorem, about bars in general.
Change 2: Slightly more information is provided about the relationship between the Fan Theorem and Bar Induction. Eventually, we should make a page about the latter.
Change 3: the section on equivalents to the fan theorem has been fixed somewhat. The section originally asserted that all of the statements provided were equivalent to the decidable fan theorem; in fact, some are equivalent to the decidable fan theorem and some to the full fan theorem.
1 to 7 of 7