topology (point-set topology, point-free topology)
see also differential topology, algebraic topology, functional analysis and topological homotopy theory
Basic concepts
fiber space, space attachment
Extra stuff, structure, properties
Kolmogorov space, Hausdorff space, regular space, normal space
sequentially compact, countably compact, locally compact, sigma-compact, paracompact, countably paracompact, strongly compact
Examples
Basic statements
closed subspaces of compact Hausdorff spaces are equivalently compact subspaces
open subspaces of compact Hausdorff spaces are locally compact
compact spaces equivalently have converging subnet of every net
continuous metric space valued function on compact metric space is uniformly continuous
paracompact Hausdorff spaces equivalently admit subordinate partitions of unity
injective proper maps to locally compact spaces are equivalently the closed embeddings
locally compact and second-countable spaces are sigma-compact
Theorems
Analysis Theorems
analysis (differential/integral calculus, functional analysis, topology)
metric space, normed vector space
open ball, open subset, neighbourhood
convergence, limit of a sequence
compactness, sequential compactness
continuous metric space valued function on compact metric space is uniformly continuous
…
…
constructive mathematics, realizability, computability
propositions as types, proofs as programs, computational trinitarianism
In classical mathematics, for metric spaces with their metric topology it is true that sequentially compact metric spaces are equivalently compact metric spaces. The analogous statement fails for more general topological spaces: for them, being sequentially compact in general neither implies nor is implied by being compact (see the counter-examples here).
But the failure of this equivalence is not due to a deficit in the concept of convergence but in the concept of sequences and sub-sequences. If the latter are generalized to nets and sub-nets (beware that the definition of sub-nets is slightly non-obvious), then the analogue of the statement remains true in classical mathematics: A topological space is compact precisely if every net in it has a sub-net that converges.
In constructive mathematics, on the other hand, this property implies the law of excluded middle, so is thus equivalent to the law of excluded middle.
(compact spaces are equivalently those for which every net has a converging subnet)
Assuming excluded middle and the axiom of choice, then:
A topological space is compact precisely if every net in has a sub-net that converges.
We break this up into lemmas and :
(in a compact space, every net has a convergent subnet)
Let be a compact topological space. Then every net in has a convergent subnet.
Let be a net. We need to show that there is a subnet which converges.
For consider the topological closures of the sets of elements of the net beyond some fixed index:
Observe that the set and hence also the set has the finite intersection property, by the fact that is a directed set. Therefore this prop. implies from the assumption of being compact that the intersection of all the is non-empty, hence that there is an element
In particular every neighbourhood of intersects each of the , and hence also each of the . By definition of the , this means that for every there exists such that , hence that is a cluster point of the net.
We will now produce a sub-net
that converges to this cluster point. To this end, we first need to build the domain directed set . Take it to be the sub-directed set of the Cartesian product directed set of with the directed neighbourhood set of
on those pairs such that the element of the net indexed by the first component is is contained in the second component:
It is clear is a preordered set. We need to check that it is indeed directed, in that every pair of elements , has a common upper bound . Now since itself is directed, there is an upper bound , and since is a cluster point of the net there is moreover an such that . Hence with we have obtained the required pair.
Next take the function to be given by
This is clearly order preserving, and it is cofinal since it is even a surjection. Hence we have defined a subnet .
It now remains to see that converges to , hence that for every open neighbourhood of we may find such that for all with and then . Now by the nature of there exists some with , and hence if we take then nature of implies that with then .
Assuming excluded middle, then:
Let be a topological space. If every net in has a subnet that converges, then is a compact topological space.
By excluded middle we may equivalently prove the contrapositive: If is not compact, then not every net in has a convergent subnet.
Hence assume that is not compact. We need to produce a net without a convergent subnet.
Again by excluded middle, then by this prop. not being compact means equivalently that there exists a set of closed subsets satisfying the finite intersection property, but such that their intersection is empty: .
Consider then , the set of finite subsets of . By the assumption that satisfies the finite intersection property, we may choose for each an element
Now regarded as a preordered set under inclusion of subsets is clearly a directed set, with an upper bound of two finite subsets given by their union. Therefore we have defined a net
We will show that this net has no converging subnet.
Assume on the contrary that there were a subnet
which converges to some .
By the assumption that , there would exist an such that , and because is a closed subset, there would exist even an open neighbourhood of such that . This would imply that for all .
Now since the function defining the subset is cofinal, there would exist such that . Moreover, by the assumption that the subnet converges, there would also be such that . Since is directed, there would then be an upper bound of these two elements. This hence satisfies both as well as . But the latter of these two means that is not in , which is a contradiction to the former. Thus we have a proof by contradiction.
In constructive mathematics, this statement is equivalent to excluded middle.
The set of two elements with its discrete topology is a compact space.
Let be an open cover of . Then there exists such that and such that . Then form a finite subcover of : the universal property of the set of two elements implies that if , then or , which means that if , then , and if , then .
Let be an inhabited subset of . Then is a directed poset: it is inhabited, it has a partial order inherited from the partial order defined on by , , , and there is an upper bound function defined for elements and as if , if , if , and if : this means that and .
Every subset inclusion of an inhabited subset is a net in .
Since is a directed poset, it follows that any function is a net in . Thus the subset inclusion is a net.
Given the set of two elements with its discrete topology, if every net in has a converging subnet, then the law of excluded middle is true.
Let be a directed set (i.e. a directed preordered set). Assume that every net in has a converging subnet, where has the discrete topology. Because the subset inclusion for any subset is a net, there is a cofinal function from to such that is a net which converges to an element , which by the universal property of satisfies either or .
Because has the discrete topology, is an open of . If , then there is an element such that , but , so .
If , then suppose that . Because is cofinal, there is an element such that , and by the definition of the partial order in , , which means that for any other element such that , , , and , which contradicts the fact that converges to . Thus, .
Thus, assuming that comes with its discrete topology, if every net in has a converging subnet, then for every inhabited subset of , either or . For the empty subset, , so for every subset of , either or .
Given any proposition , let us define the subset of as
It follows that if , then , and if , then . Thus, the law of excluded middle is true for all propositions .
Last revised on July 24, 2024 at 21:16:47. See the history of this page for a list of all contributions to it.