Definition df-ldlf

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)

	Ref	Expression
Assertion	df-ldlf	$$⊢\mathrm{Ldlf}=\mathrm{CovHasRef}\left\{x|x\preccurlyeq \mathrm{\omega }\right\}$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cldlf	$$class\mathrm{Ldlf}$$
1		vx	$$setvarx$$
2	1	cv	$$setvarx$$
3		cdom	$$class\preccurlyeq$$
4		com	$$class\mathrm{\omega }$$
5	2 4 3	wbr	$$wffx\preccurlyeq \mathrm{\omega }$$
6	5 1	cab	$$class\left\{x|x\preccurlyeq \mathrm{\omega }\right\}$$
7	6	ccref	$$class\mathrm{CovHasRef}\left\{x|x\preccurlyeq \mathrm{\omega }\right\}$$
8	0 7	wceq	$$wff\mathrm{Ldlf}=\mathrm{CovHasRef}\left\{x|x\preccurlyeq \mathrm{\omega }\right\}$$