Definition df-nlly 21270

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 sub-neighborhood 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 𝑛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.)

Assertion

Ref	Expression
df-nlly	|- 𝑛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 }

Distinct variable group:   u, j, x, y, A

Detailed syntax breakdown of Definition df-nlly

Step	Hyp	Ref	Expression
1		cA	. . 3 class A
2	1	cnlly 21268	. 2 class 𝑛Locally A
3		vj	. . . . . . . . 9 setvar j
4	3	cv 1482	. . . . . . . 8 class j
5		vu	. . . . . . . . 9 setvar u
6	5	cv 1482	. . . . . . . 8 class u
7		crest 16081	. . . . . . . 8 class ↾t
8	4, 6, 7	co 6650	. . . . . . 7 class ( j ↾t u )
9	8, 1	wcel 1990	. . . . . 6 wff ( j ↾t u ) e. A
10		vy	. . . . . . . . . 10 setvar y
11	10	cv 1482	. . . . . . . . 9 class y
12	11	csn 4177	. . . . . . . 8 class { y }
13		cnei 20901	. . . . . . . . 9 class nei
14	4, 13	cfv 5888	. . . . . . . 8 class ( nei ` j )
15	12, 14	cfv 5888	. . . . . . 7 class ( ( nei ` j ) ` { y } )
16		vx	. . . . . . . . 9 setvar x
17	16	cv 1482	. . . . . . . 8 class x
18	17	cpw 4158	. . . . . . 7 class ~P x
19	15, 18	cin 3573	. . . . . 6 class ( ( ( nei ` j ) ` { y } ) i^i ~P x )
20	9, 5, 19	wrex 2913	. . . . 5 wff E. u e. ( ( ( nei ` j ) ` { y } ) i^i ~P x ) ( j ↾t u ) e. A
21	20, 10, 17	wral 2912	. . . 4 wff A. y e. x E. u e. ( ( ( nei ` j ) ` { y } ) i^i ~P x ) ( j ↾t u ) e. A
22	21, 16, 4	wral 2912	. . 3 wff A. x e. j A. y e. x E. u e. ( ( ( nei ` j ) ` { y } ) i^i ~P x ) ( j ↾t u ) e. A
23		ctop 20698	. . 3 class Top
24	22, 3, 23	crab 2916	. 2 class { 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 }
25	2, 24	wceq 1483	1 wff 𝑛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 }

This definition is referenced by:  isnlly  21272  nllyeq  21274