Description: Every open cover of a Compact space has a finite refinement. (Contributed by Thierry Arnoux, 1-Feb-2020)
Ref | Expression | ||
---|---|---|---|
Hypothesis | cmpfiref.x | ||
Assertion | cmpfiref |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cmpfiref.x | ||
2 | cmpcref | ||
3 | id | ||
4 | 1 2 3 | crefdf |