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 { 𝑥 ∣ 𝑥 ≼ ω }

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cldlf	⊢ Ldlf
1		vx	⊢ 𝑥
2	1	cv	⊢ 𝑥
3		cdom	⊢ ≼
4		com	⊢ ω
5	2 4 3	wbr	⊢ 𝑥 ≼ ω
6	5 1	cab	⊢ { 𝑥 ∣ 𝑥 ≼ ω }
7	6	ccref	⊢ CovHasRef { 𝑥 ∣ 𝑥 ≼ ω }
8	0 7	wceq	⊢ Ldlf = CovHasRef { 𝑥 ∣ 𝑥 ≼ ω }