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

Definition df-ldlf 29054
Description: Definition of a Lindelöf space. A Lindelöf space is a topological space in which every open cover has a countable subcover. Definition 1 of [BourbakiTop2] p. 195. (Contributed by Thierry Arnoux, 30-Jan-2020.)
Assertion
Ref Expression
df-ldlf Ldlf = CovHasRef{𝑥𝑥 ≼ ω}

Detailed syntax breakdown of Definition df-ldlf
StepHypRef Expression
1 cldlf 29053 . 2 class Ldlf
2 vx . . . . . 6 setvar 𝑥
32cv 1473 . . . . 5 class 𝑥
4 com 6934 . . . . 5 class ω
5 cdom 7816 . . . . 5 class
63, 4, 5wbr 4577 . . . 4 wff 𝑥 ≼ ω
76, 2cab 2595 . . 3 class {𝑥𝑥 ≼ ω}
87ccref 29043 . 2 class CovHasRef{𝑥𝑥 ≼ ω}
91, 8wceq 1474 1 wff Ldlf = CovHasRef{𝑥𝑥 ≼ ω}
Colors of variables: wff setvar class
This definition is referenced by:  ldlfcntref  29055
  Copyright terms: Public domain W3C validator