Description: A topology generated by a basis is compact iff open covers drawn from the basis have finite subcovers. (See also alexsub , which further specializes to subbases, assuming the ultrafilter lemma.) (Contributed by Mario Carneiro, 26-Aug-2015)
Ref | Expression | ||
---|---|---|---|
Assertion | tgcmp | |