Let be a site, and let be a subcategory of . A manifold of type consists of the aforementioned site together with a class of isomorphisms of , where the 's are open in and the are objects of , such that
for all there is a covering of such that for each , there exists an with and
whenever st. and consitute a covering and and belong to the class , the maps and guaranteed by the universal property of the pullback are isomorphisms onto their respective images and is a morphism of .
Let be a logical statement, whose arguments are a topological manifold and a closed subset . Suppose that the following are true:
Whenever is compact and convex, where is a coördinate chart on , then is true
Whenever and are true, then is true
Whenever is a descending chain of compact subsets of , is true for all , then is true
Whenever is true for all relatively compact, open , then is true
Then for all closed , is true.
Proof: First we prove by induction on that for all sets of the type for certain compact convex (), the statement is true. We proceed by induction on . For , the statement is implied by the first assumption. Suppose now that is true. Note that also is true by the first assumption. Also
and , where is compact and convex as the intersection of two compact and convex sets. Thus, since the sets are only many, by induction on , we may also conclude that holds. By 2., we conclude .
Now, we prove that is true whenever is a compact subset of a set of the type , where is compact and convex. Indeed, for each , cover by all the cubes of sidelength centered at the points of that intersect it. Then set
, so that .
By the second assumption, holds for each , and hence by the third assumption holds.
Now we claim by induction on that whenever are compact subsets of sets of the type ( compact and convex), then holds. For , this follows from what we just proved. For the induction step, suppose that holds. Note that also holds by what we just proved. Then we have
and since is a compact subset of , holds by what we just proved, and therefore, by induction, holds. Hence, by 2., we get that is true.
Now we are ready to prove that is true whenever is compact. Indeed, let be compact. Then cover by sets , where are some charts and is compact and convex. By compactness of , we may extract a finite subcover . By intersecting with and retaining compactness (as the intersection of two compact sets is compact), we may assume that are contained within and in particular