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 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 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 21078 | . 2 class 𝑛-Locally 𝐴 |
3 | vj | . . . . . . . . 9 setvar 𝑗 | |
4 | 3 | cv 1474 | . . . . . . . 8 class 𝑗 |
5 | vu | . . . . . . . . 9 setvar 𝑢 | |
6 | 5 | cv 1474 | . . . . . . . 8 class 𝑢 |
7 | crest 15904 | . . . . . . . 8 class ↾t | |
8 | 4, 6, 7 | co 6549 | . . . . . . 7 class (𝑗 ↾t 𝑢) |
9 | 8, 1 | wcel 1977 | . . . . . 6 wff (𝑗 ↾t 𝑢) ∈ 𝐴 |
10 | vy | . . . . . . . . . 10 setvar 𝑦 | |
11 | 10 | cv 1474 | . . . . . . . . 9 class 𝑦 |
12 | 11 | csn 4125 | . . . . . . . 8 class {𝑦} |
13 | cnei 20711 | . . . . . . . . 9 class nei | |
14 | 4, 13 | cfv 5804 | . . . . . . . 8 class (nei‘𝑗) |
15 | 12, 14 | cfv 5804 | . . . . . . 7 class ((nei‘𝑗)‘{𝑦}) |
16 | vx | . . . . . . . . 9 setvar 𝑥 | |
17 | 16 | cv 1474 | . . . . . . . 8 class 𝑥 |
18 | 17 | cpw 4108 | . . . . . . 7 class 𝒫 𝑥 |
19 | 15, 18 | cin 3539 | . . . . . 6 class (((nei‘𝑗)‘{𝑦}) ∩ 𝒫 𝑥) |
20 | 9, 5, 19 | wrex 2897 | . . . . 5 wff ∃𝑢 ∈ (((nei‘𝑗)‘{𝑦}) ∩ 𝒫 𝑥)(𝑗 ↾t 𝑢) ∈ 𝐴 |
21 | 20, 10, 17 | wral 2896 | . . . 4 wff ∀𝑦 ∈ 𝑥 ∃𝑢 ∈ (((nei‘𝑗)‘{𝑦}) ∩ 𝒫 𝑥)(𝑗 ↾t 𝑢) ∈ 𝐴 |
22 | 21, 16, 4 | wral 2896 | . . 3 wff ∀𝑥 ∈ 𝑗 ∀𝑦 ∈ 𝑥 ∃𝑢 ∈ (((nei‘𝑗)‘{𝑦}) ∩ 𝒫 𝑥)(𝑗 ↾t 𝑢) ∈ 𝐴 |
23 | ctop 20517 | . . 3 class Top | |
24 | 22, 3, 23 | crab 2900 | . 2 class {𝑗 ∈ Top ∣ ∀𝑥 ∈ 𝑗 ∀𝑦 ∈ 𝑥 ∃𝑢 ∈ (((nei‘𝑗)‘{𝑦}) ∩ 𝒫 𝑥)(𝑗 ↾t 𝑢) ∈ 𝐴} |
25 | 2, 24 | wceq 1475 | 1 wff 𝑛-Locally 𝐴 = {𝑗 ∈ Top ∣ ∀𝑥 ∈ 𝑗 ∀𝑦 ∈ 𝑥 ∃𝑢 ∈ (((nei‘𝑗)‘{𝑦}) ∩ 𝒫 𝑥)(𝑗 ↾t 𝑢) ∈ 𝐴} |
Colors of variables: wff setvar class |
This definition is referenced by: isnlly 21082 nllyeq 21084 |
Copyright terms: Public domain | W3C validator |