Definition df-ldlf 31206

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

Step	Hyp	Ref	Expression
1		cldlf 31205	. 2 class Ldlf
2		vx	. . . . . 6 setvar 𝑥
3	2	cv 1537	. . . . 5 class 𝑥
4		com 7560	. . . . 5 class ω
5		cdom 8490	. . . . 5 class ≼
6	3, 4, 5	wbr 5030	. . . 4 wff 𝑥 ≼ ω
7	6, 2	cab 2776	. . 3 class {𝑥 ∣ 𝑥 ≼ ω}
8	7	ccref 31195	. 2 class CovHasRef{𝑥 ∣ 𝑥 ≼ ω}
9	1, 8	wceq 1538	1 wff Ldlf = CovHasRef{𝑥 ∣ 𝑥 ≼ ω}

This definition is referenced by:  ldlfcntref  31207