Users' Mathboxes Mathbox for Thierry Arnoux < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-pcmp Structured version   Visualization version   GIF version

Definition df-pcmp 29057
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.)
Assertion
Ref Expression
df-pcmp Paracomp = {𝑗𝑗 ∈ CovHasRef(LocFin‘𝑗)}

Detailed syntax breakdown of Definition df-pcmp
StepHypRef Expression
1 cpcmp 29056 . 2 class Paracomp
2 vj . . . . 5 setvar 𝑗
32cv 1473 . . . 4 class 𝑗
4 clocfin 21059 . . . . . 6 class LocFin
53, 4cfv 5790 . . . . 5 class (LocFin‘𝑗)
65ccref 29043 . . . 4 class CovHasRef(LocFin‘𝑗)
73, 6wcel 1976 . . 3 wff 𝑗 ∈ CovHasRef(LocFin‘𝑗)
87, 2cab 2595 . 2 class {𝑗𝑗 ∈ CovHasRef(LocFin‘𝑗)}
91, 8wceq 1474 1 wff Paracomp = {𝑗𝑗 ∈ CovHasRef(LocFin‘𝑗)}
Colors of variables: wff setvar class
This definition is referenced by:  ispcmp  29058
  Copyright terms: Public domain W3C validator