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.
For proposition 3.2 (continuous functions detected by nets), it seems that the first direction of the proof doesn’t use excluded middle. The other direction has two proofs, one of which doesn’t use excluded middle. If this is all correct, this means that one doesn’t have to assume excluded middle to prove proposition 3.2, which means that the assumption of excluded middle in the theorem can be removed.
Anonymouse
1 to 2 of 2