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	|- Ldlf = CovHasRef { x | x ~<_ _om }

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cldlf	|- Ldlf
1		vx	|- x
2	1	cv	|- x
3		cdom	|- ~<_
4		com	|- _om
5	2 4 3	wbr	|- x ~<_ _om
6	5 1	cab	|- { x | x ~<_ _om }
7	6	ccref	|- CovHasRef { x | x ~<_ _om }
8	0 7	wceq	|- Ldlf = CovHasRef { x | x ~<_ _om }