Vertex-star cover obstruction to compactness (source code)

= Vertex-star cover obstruction to compactness

The <topological realization> of a <simplicial complex> with infinitely many <vertices> is not <compact>. Its vertex <open star in a simplicial complex> form an <open cover>, but a vertex belongs only to its own star. Thus every finite collection of vertex stars omits all the other vertices. The argument uses the <weak topology of a simplicial realization>, in which a vertex star is <open> because its complement is the realization of the subcomplex of simplices missing that vertex. No local finiteness assumption is required.