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

Definition df-nlly 17522
 Description: Define a space that is n-locally , where is a topological property like "compact", "connected", or "path-connected". A topological space is n-locally if every neighborhood of a point contains a sub-neighborhood that is in the subspace topology. The terminology "n-locally", where 'n' stands for "neighborhood", is not standard, although this is sometimes called "weakly locally ". The reason for the distinction is that some notions only make sense for arbitrary neighborhoods (such as "locally compact", which is actually 𝑛Locally 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 t
Distinct variable group:   ,,,,

Detailed syntax breakdown of Definition df-nlly
StepHypRef Expression
1 cA . . 3
21cnlly 17520 . 2 𝑛Locally
3 vj . . . . . . . . 9
43cv 1651 . . . . . . . 8
5 vu . . . . . . . . 9
65cv 1651 . . . . . . . 8
7 crest 13640 . . . . . . . 8 t
84, 6, 7co 6073 . . . . . . 7 t
98, 1wcel 1725 . . . . . 6 t
10 vy . . . . . . . . . 10
1110cv 1651 . . . . . . . . 9
1211csn 3806 . . . . . . . 8
13 cnei 17153 . . . . . . . . 9
144, 13cfv 5446 . . . . . . . 8
1512, 14cfv 5446 . . . . . . 7
16 vx . . . . . . . . 9
1716cv 1651 . . . . . . . 8
1817cpw 3791 . . . . . . 7
1915, 18cin 3311 . . . . . 6
209, 5, 19wrex 2698 . . . . 5 t
2120, 10, 17wral 2697 . . . 4 t
2221, 16, 4wral 2697 . . 3 t
23 ctop 16950 . . 3
2422, 3, 23crab 2701 . 2 t
252, 24wceq 1652 1 𝑛Locally t
 Colors of variables: wff set class This definition is referenced by:  isnlly  17524  nllyeq  17526
 Copyright terms: Public domain W3C validator