Metamath Proof Explorer

Definition df-pcmp

Description: Definition of a paracompact topology. A topology is said to be paracompact iff every open cover has an open refinement that is locally finite. The definition 6 of BourbakiTop1 p. I.69. also requires the topology to be Hausdorff, but this is dropped here. (Contributed by Thierry Arnoux, 7-Jan-2020)

Ref Expression
Assertion df-pcmp Paracomp = j | j CovHasRef LocFin j

Detailed syntax breakdown

Step Hyp Ref Expression
0 cpcmp class Paracomp
1 vj setvar j
2 1 cv setvar j
3 clocfin class LocFin
4 2 3 cfv class LocFin j
5 4 ccref class CovHasRef LocFin j
6 2 5 wcel wff j CovHasRef LocFin j
7 6 1 cab class j | j CovHasRef LocFin j
8 0 7 wceq wff Paracomp = j | j CovHasRef LocFin j