Definition df-ldlf 29920

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 { x | x ~<_ om }

Detailed syntax breakdown of Definition df-ldlf

Step	Hyp	Ref	Expression
1		cldlf 29919	. 2 class Ldlf
2		vx	. . . . . 6 setvar x
3	2	cv 1482	. . . . 5 class x
4		com 7065	. . . . 5 class om
5		cdom 7953	. . . . 5 class ~<_
6	3, 4, 5	wbr 4653	. . . 4 wff x ~<_ om
7	6, 2	cab 2608	. . 3 class { x | x ~<_ om }
8	7	ccref 29909	. 2 class CovHasRef { x | x ~<_ om }
9	1, 8	wceq 1483	1 wff Ldlf = CovHasRef { x | x ~<_ om }

This definition is referenced by:  ldlfcntref  29921