# Metamath Proof Explorer

## 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}=\left\{{j}\in \mathrm{Top}|\forall {x}\in {j}\phantom{\rule{.4em}{0ex}}\right\}$

### Detailed syntax breakdown

Step Hyp Ref Expression
0 cA ${class}{A}$
1 0 cnlly ${class}N-Locally{A}$
2 vj ${setvar}{j}$
3 ctop ${class}\mathrm{Top}$
4 vx ${setvar}{x}$
5 2 cv ${setvar}{j}$
6 vy ${setvar}{y}$
7 4 cv ${setvar}{x}$
8 vu ${setvar}{u}$
9 cnei ${class}\mathrm{nei}$
10 5 9 cfv ${class}\mathrm{nei}\left({j}\right)$
11 6 cv ${setvar}{y}$
12 11 csn ${class}\left\{{y}\right\}$
13 12 10 cfv ${class}\mathrm{nei}\left({j}\right)\left(\left\{{y}\right\}\right)$
14 7 cpw ${class}𝒫{x}$
15 13 14 cin ${class}\left(\mathrm{nei}\left({j}\right)\left(\left\{{y}\right\}\right)\cap 𝒫{x}\right)$
16 crest ${class}{↾}_{𝑡}$
17 8 cv ${setvar}{u}$
18 5 17 16 co ${class}\left({j}{↾}_{𝑡}{u}\right)$
19 18 0 wcel ${wff}{j}{↾}_{𝑡}{u}\in {A}$
20 19 8 15 wrex ${wff}\exists {u}\in \left(\mathrm{nei}\left({j}\right)\left(\left\{{y}\right\}\right)\cap 𝒫{x}\right)\phantom{\rule{.4em}{0ex}}{j}{↾}_{𝑡}{u}\in {A}$
21 20 6 7 wral ${wff}\forall {y}\in {x}\phantom{\rule{.4em}{0ex}}\exists {u}\in \left(\mathrm{nei}\left({j}\right)\left(\left\{{y}\right\}\right)\cap 𝒫{x}\right)\phantom{\rule{.4em}{0ex}}{j}{↾}_{𝑡}{u}\in {A}$
22 21 4 5 wral ${wff}\forall {x}\in {j}\phantom{\rule{.4em}{0ex}}\forall {y}\in {x}\phantom{\rule{.4em}{0ex}}\exists {u}\in \left(\mathrm{nei}\left({j}\right)\left(\left\{{y}\right\}\right)\cap 𝒫{x}\right)\phantom{\rule{.4em}{0ex}}{j}{↾}_{𝑡}{u}\in {A}$
23 22 2 3 crab ${class}\left\{{j}\in \mathrm{Top}|\forall {x}\in {j}\phantom{\rule{.4em}{0ex}}\forall {y}\in {x}\phantom{\rule{.4em}{0ex}}\exists {u}\in \left(\mathrm{nei}\left({j}\right)\left(\left\{{y}\right\}\right)\cap 𝒫{x}\right)\phantom{\rule{.4em}{0ex}}{j}{↾}_{𝑡}{u}\in {A}\right\}$
24 1 23 wceq ${wff}N-Locally{A}=\left\{{j}\in \mathrm{Top}|\forall {x}\in {j}\phantom{\rule{.4em}{0ex}}\right\}$