Definition df-nlly

Description: Define a space that is n-locally A , where A is a topological property like "compact", "connected", or "path-connected". A topological space is n-locally A if every neighborhood of a point contains a subneighborhood that is A in the subspace topology.

The terminology "n-locally", where 'n' stands for "neighborhood", is not standard, although this is sometimes called "weakly locally A ". The reason for the distinction is that some notions only make sense for arbitrary neighborhoods (such as "locally compact", which is actually N-Locally Comp in our terminology - open compact sets are not very useful), while others such as "locally connected" are strictly weaker notions if the neighborhoods are not required to be open. (Contributed by Mario Carneiro, 2-Mar-2015)

	Ref	Expression
Assertion	df-nlly	|- N-Locally A = { j e. Top | A. x e. j A. y e. x E. u e. ( ( ( nei ` j ) ` { y } ) i^i ~P x ) ( j |`t u ) e. A }

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cA	|- A
1	0	cnlly	|- N-Locally A
2		vj	|- j
3		ctop	|- Top
4		vx	|- x
5	2	cv	|- j
6		vy	|- y
7	4	cv	|- x
8		vu	|- u
9		cnei	|- nei
10	5 9	cfv	|- ( nei ` j )
11	6	cv	|- y
12	11	csn	|- { y }
13	12 10	cfv	|- ( ( nei ` j ) ` { y } )
14	7	cpw	|- ~P x
15	13 14	cin	|- ( ( ( nei ` j ) ` { y } ) i^i ~P x )
16		crest	|- |`t
17	8	cv	|- u
18	5 17 16	co	|- ( j |`t u )
19	18 0	wcel	|- ( j |`t u ) e. A
20	19 8 15	wrex	|- E. u e. ( ( ( nei ` j ) ` { y } ) i^i ~P x ) ( j |`t u ) e. A
21	20 6 7	wral	|- A. y e. x E. u e. ( ( ( nei ` j ) ` { y } ) i^i ~P x ) ( j |`t u ) e. A
22	21 4 5	wral	|- A. x e. j A. y e. x E. u e. ( ( ( nei ` j ) ` { y } ) i^i ~P x ) ( j |`t u ) e. A
23	22 2 3	crab	|- { j e. Top | A. x e. j A. y e. x E. u e. ( ( ( nei ` j ) ` { y } ) i^i ~P x ) ( j |`t u ) e. A }
24	1 23	wceq	|- N-Locally A = { j e. Top | A. x e. j A. y e. x E. u e. ( ( ( nei ` j ) ` { y } ) i^i ~P x ) ( j |`t u ) e. A }