![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > df-nlly | Structured version Visualization version GIF version |
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 subneighborhood 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 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 |
---|---|
df-nlly | ⊢ 𝑛-Locally 𝐴 = {𝑗 ∈ Top ∣ ∀𝑥 ∈ 𝑗 ∀𝑦 ∈ 𝑥 ∃𝑢 ∈ (((nei‘𝑗)‘{𝑦}) ∩ 𝒫 𝑥)(𝑗 ↾t 𝑢) ∈ 𝐴} |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cA | . . 3 class 𝐴 | |
2 | 1 | cnlly 22938 | . 2 class 𝑛-Locally 𝐴 |
3 | vj | . . . . . . . . 9 setvar 𝑗 | |
4 | 3 | cv 1541 | . . . . . . . 8 class 𝑗 |
5 | vu | . . . . . . . . 9 setvar 𝑢 | |
6 | 5 | cv 1541 | . . . . . . . 8 class 𝑢 |
7 | crest 17353 | . . . . . . . 8 class ↾t | |
8 | 4, 6, 7 | co 7396 | . . . . . . 7 class (𝑗 ↾t 𝑢) |
9 | 8, 1 | wcel 2107 | . . . . . 6 wff (𝑗 ↾t 𝑢) ∈ 𝐴 |
10 | vy | . . . . . . . . . 10 setvar 𝑦 | |
11 | 10 | cv 1541 | . . . . . . . . 9 class 𝑦 |
12 | 11 | csn 4624 | . . . . . . . 8 class {𝑦} |
13 | cnei 22570 | . . . . . . . . 9 class nei | |
14 | 4, 13 | cfv 6535 | . . . . . . . 8 class (nei‘𝑗) |
15 | 12, 14 | cfv 6535 | . . . . . . 7 class ((nei‘𝑗)‘{𝑦}) |
16 | vx | . . . . . . . . 9 setvar 𝑥 | |
17 | 16 | cv 1541 | . . . . . . . 8 class 𝑥 |
18 | 17 | cpw 4598 | . . . . . . 7 class 𝒫 𝑥 |
19 | 15, 18 | cin 3945 | . . . . . 6 class (((nei‘𝑗)‘{𝑦}) ∩ 𝒫 𝑥) |
20 | 9, 5, 19 | wrex 3071 | . . . . 5 wff ∃𝑢 ∈ (((nei‘𝑗)‘{𝑦}) ∩ 𝒫 𝑥)(𝑗 ↾t 𝑢) ∈ 𝐴 |
21 | 20, 10, 17 | wral 3062 | . . . 4 wff ∀𝑦 ∈ 𝑥 ∃𝑢 ∈ (((nei‘𝑗)‘{𝑦}) ∩ 𝒫 𝑥)(𝑗 ↾t 𝑢) ∈ 𝐴 |
22 | 21, 16, 4 | wral 3062 | . . 3 wff ∀𝑥 ∈ 𝑗 ∀𝑦 ∈ 𝑥 ∃𝑢 ∈ (((nei‘𝑗)‘{𝑦}) ∩ 𝒫 𝑥)(𝑗 ↾t 𝑢) ∈ 𝐴 |
23 | ctop 22364 | . . 3 class Top | |
24 | 22, 3, 23 | crab 3433 | . 2 class {𝑗 ∈ Top ∣ ∀𝑥 ∈ 𝑗 ∀𝑦 ∈ 𝑥 ∃𝑢 ∈ (((nei‘𝑗)‘{𝑦}) ∩ 𝒫 𝑥)(𝑗 ↾t 𝑢) ∈ 𝐴} |
25 | 2, 24 | wceq 1542 | 1 wff 𝑛-Locally 𝐴 = {𝑗 ∈ Top ∣ ∀𝑥 ∈ 𝑗 ∀𝑦 ∈ 𝑥 ∃𝑢 ∈ (((nei‘𝑗)‘{𝑦}) ∩ 𝒫 𝑥)(𝑗 ↾t 𝑢) ∈ 𝐴} |
Colors of variables: wff setvar class |
This definition is referenced by: isnlly 22942 nllyeq 22944 |
Copyright terms: Public domain | W3C validator |