MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-nlly Unicode version

Definition df-nlly 17193
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 because some notions only make sense for arbitrary neighborhoods (such as "locally compact", which is actually 𝑛Locally 
Comp in our teminology - 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 ) ( jt  u )  e.  A }
Distinct variable group:    u, j, x, y, A

Detailed syntax breakdown of Definition df-nlly
StepHypRef Expression
1 cA . . 3  class  A
21cnlly 17191 . 2  class 𝑛Locally  A
3 vj . . . . . . . . 9  set  j
43cv 1622 . . . . . . . 8  class  j
5 vu . . . . . . . . 9  set  u
65cv 1622 . . . . . . . 8  class  u
7 crest 13325 . . . . . . . 8  classt
84, 6, 7co 5858 . . . . . . 7  class  ( jt  u )
98, 1wcel 1684 . . . . . 6  wff  ( jt  u )  e.  A
10 vy . . . . . . . . . 10  set  y
1110cv 1622 . . . . . . . . 9  class  y
1211csn 3640 . . . . . . . 8  class  { y }
13 cnei 16834 . . . . . . . . 9  class  nei
144, 13cfv 5255 . . . . . . . 8  class  ( nei `  j )
1512, 14cfv 5255 . . . . . . 7  class  ( ( nei `  j ) `
 { y } )
16 vx . . . . . . . . 9  set  x
1716cv 1622 . . . . . . . 8  class  x
1817cpw 3625 . . . . . . 7  class  ~P x
1915, 18cin 3151 . . . . . 6  class  ( ( ( nei `  j
) `  { y } )  i^i  ~P x )
209, 5, 19wrex 2544 . . . . 5  wff  E. u  e.  ( ( ( nei `  j ) `  {
y } )  i^i 
~P x ) ( jt  u )  e.  A
2120, 10, 17wral 2543 . . . 4  wff  A. y  e.  x  E. u  e.  ( ( ( nei `  j ) `  {
y } )  i^i 
~P x ) ( jt  u )  e.  A
2221, 16, 4wral 2543 . . 3  wff  A. x  e.  j  A. y  e.  x  E. u  e.  ( ( ( nei `  j ) `  {
y } )  i^i 
~P x ) ( jt  u )  e.  A
23 ctop 16631 . . 3  class  Top
2422, 3, 23crab 2547 . 2  class  { j  e.  Top  |  A. x  e.  j  A. y  e.  x  E. u  e.  ( (
( nei `  j
) `  { y } )  i^i  ~P x ) ( jt  u )  e.  A }
252, 24wceq 1623 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 ) ( jt  u )  e.  A }
Colors of variables: wff set class
This definition is referenced by:  isnlly  17195  nllyeq  17197
  Copyright terms: Public domain W3C validator