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
…
…
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
Using excluded middle and dependent choice then:
Let be a metric space which is sequentially compact. Then it is totally bounded metric space.
Assume that were not totally bounded. This would mean that there existed a positive real number such that for every finite subset we had that is not the union of the open balls of radius around the elements of this finite subset
This would mean that we could inductively choose elements
This constituted a sequence , and by assumption of sequential compactness this would have a converging sub-sequence. But this would then be a contradiction, since by the above assumption that is not totally bounded we have for all . Hence we have a proof by contradiction that in fact is totally bounded.
Last revised on June 26, 2019 at 11:20:05. See the history of this page for a list of all contributions to it.