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

Definition df-nlly 20413
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 ) ( 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 20411 . 2  class 𝑛Locally  A
3 vj . . . . . . . . 9  setvar  j
43cv 1436 . . . . . . . 8  class  j
5 vu . . . . . . . . 9  setvar  u
65cv 1436 . . . . . . . 8  class  u
7 crest 15278 . . . . . . . 8  classt
84, 6, 7co 6305 . . . . . . 7  class  ( jt  u )
98, 1wcel 1870 . . . . . 6  wff  ( jt  u )  e.  A
10 vy . . . . . . . . . 10  setvar  y
1110cv 1436 . . . . . . . . 9  class  y
1211csn 4002 . . . . . . . 8  class  { y }
13 cnei 20044 . . . . . . . . 9  class  nei
144, 13cfv 5601 . . . . . . . 8  class  ( nei `  j )
1512, 14cfv 5601 . . . . . . 7  class  ( ( nei `  j ) `
 { y } )
16 vx . . . . . . . . 9  setvar  x
1716cv 1436 . . . . . . . 8  class  x
1817cpw 3985 . . . . . . 7  class  ~P x
1915, 18cin 3441 . . . . . 6  class  ( ( ( nei `  j
) `  { y } )  i^i  ~P x )
209, 5, 19wrex 2783 . . . . 5  wff  E. u  e.  ( ( ( nei `  j ) `  {
y } )  i^i 
~P x ) ( jt  u )  e.  A
2120, 10, 17wral 2782 . . . 4  wff  A. y  e.  x  E. u  e.  ( ( ( nei `  j ) `  {
y } )  i^i 
~P x ) ( jt  u )  e.  A
2221, 16, 4wral 2782 . . 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 19848 . . 3  class  Top
2422, 3, 23crab 2786 . 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 1437 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 setvar class
This definition is referenced by:  isnlly  20415  nllyeq  20417
  Copyright terms: Public domain W3C validator