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 32494
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 32493 . 2 class Paracomp
2 vj . . . . 5 setvar 𝑗
32cv 1541 . . . 4 class 𝑗
4 clocfin 22871 . . . . . 6 class LocFin
53, 4cfv 6497 . . . . 5 class (LocFinβ€˜π‘—)
65ccref 32480 . . . 4 class CovHasRef(LocFinβ€˜π‘—)
73, 6wcel 2107 . . 3 wff 𝑗 ∈ CovHasRef(LocFinβ€˜π‘—)
87, 2cab 2710 . 2 class {𝑗 ∣ 𝑗 ∈ CovHasRef(LocFinβ€˜π‘—)}
91, 8wceq 1542 1 wff Paracomp = {𝑗 ∣ 𝑗 ∈ CovHasRef(LocFinβ€˜π‘—)}
Colors of variables: wff setvar class
This definition is referenced by:  ispcmp  32495
  Copyright terms: Public domain W3C validator