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.
I created a short entry Banach-Alaoglu theorem to fulfil a grey link. While the general theorem is equivalent to the Tychonoff theorem for Hausdorff spaces, the case of separable Banach spaces is constructive. I do wonder how constructive, but apparently this gets used to construct solutions to PDEs, so I guess it’s quite concrete.
Perhaps it’s worth noting that even in the non-separable case the Axiom of choice is not required for the proof: it bases on the product . As discussed here in Remark 2.1 Tychonoff’s theorem holds without AC in this case as is Hausdorff.
You still need the ultrafilter principle/theorem though, which is where I found the needed link to the page on the B-A theorem.
Thank you, I wasn’t aware of this subtlety. But what about this rescue of Tychonov’s theorem:
In the case of an product of intervals we use Definition 2.5:
For the second step: take any neighborhood of . It contains a neighborhood of some cluster point of . Hence the intersection of any set in with is inhabited.
For the last step in this argument: it is obvious that for any neighborhood belonging to the subbase of the topology of consisting of all preimages of all open sets under all projection maps it holds that has nonempty intersection with every as is inhabited. This holds also for finite intersection . Finally, it holds for products.
Wait, are you claiming that the Tychonoff theorem for products of intervals doesn’t require the ultrafilter principle?
I think the ultrafilter principle should follow from the Tychonoff theorem for intervals. If the power is compact for any set , then so is the power (being a closed subspace). But it is not hard to prove the Boolean prime ideal theorem from compactness of , and this is equivalent to the ultrafilter principle.
You are right. The last step in my proof is actually wrong.
I’ve added some links to the constructive literature, both Bishop and locales. I haven’t traced everything back to the original sources yet.
Thanks, Bas!
1 to 8 of 8