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 22067 | . 2 class 𝑛-Locally 𝐴 |
3 | vj | . . . . . . . . 9 setvar 𝑗 | |
4 | 3 | cv 1532 | . . . . . . . 8 class 𝑗 |
5 | vu | . . . . . . . . 9 setvar 𝑢 | |
6 | 5 | cv 1532 | . . . . . . . 8 class 𝑢 |
7 | crest 16688 | . . . . . . . 8 class ↾t | |
8 | 4, 6, 7 | co 7150 | . . . . . . 7 class (𝑗 ↾t 𝑢) |
9 | 8, 1 | wcel 2110 | . . . . . 6 wff (𝑗 ↾t 𝑢) ∈ 𝐴 |
10 | vy | . . . . . . . . . 10 setvar 𝑦 | |
11 | 10 | cv 1532 | . . . . . . . . 9 class 𝑦 |
12 | 11 | csn 4561 | . . . . . . . 8 class {𝑦} |
13 | cnei 21699 | . . . . . . . . 9 class nei | |
14 | 4, 13 | cfv 6350 | . . . . . . . 8 class (nei‘𝑗) |
15 | 12, 14 | cfv 6350 | . . . . . . 7 class ((nei‘𝑗)‘{𝑦}) |
16 | vx | . . . . . . . . 9 setvar 𝑥 | |
17 | 16 | cv 1532 | . . . . . . . 8 class 𝑥 |
18 | 17 | cpw 4539 | . . . . . . 7 class 𝒫 𝑥 |
19 | 15, 18 | cin 3935 | . . . . . 6 class (((nei‘𝑗)‘{𝑦}) ∩ 𝒫 𝑥) |
20 | 9, 5, 19 | wrex 3139 | . . . . 5 wff ∃𝑢 ∈ (((nei‘𝑗)‘{𝑦}) ∩ 𝒫 𝑥)(𝑗 ↾t 𝑢) ∈ 𝐴 |
21 | 20, 10, 17 | wral 3138 | . . . 4 wff ∀𝑦 ∈ 𝑥 ∃𝑢 ∈ (((nei‘𝑗)‘{𝑦}) ∩ 𝒫 𝑥)(𝑗 ↾t 𝑢) ∈ 𝐴 |
22 | 21, 16, 4 | wral 3138 | . . 3 wff ∀𝑥 ∈ 𝑗 ∀𝑦 ∈ 𝑥 ∃𝑢 ∈ (((nei‘𝑗)‘{𝑦}) ∩ 𝒫 𝑥)(𝑗 ↾t 𝑢) ∈ 𝐴 |
23 | ctop 21495 | . . 3 class Top | |
24 | 22, 3, 23 | crab 3142 | . 2 class {𝑗 ∈ Top ∣ ∀𝑥 ∈ 𝑗 ∀𝑦 ∈ 𝑥 ∃𝑢 ∈ (((nei‘𝑗)‘{𝑦}) ∩ 𝒫 𝑥)(𝑗 ↾t 𝑢) ∈ 𝐴} |
25 | 2, 24 | wceq 1533 | 1 wff 𝑛-Locally 𝐴 = {𝑗 ∈ Top ∣ ∀𝑥 ∈ 𝑗 ∀𝑦 ∈ 𝑥 ∃𝑢 ∈ (((nei‘𝑗)‘{𝑦}) ∩ 𝒫 𝑥)(𝑗 ↾t 𝑢) ∈ 𝐴} |
Colors of variables: wff setvar class |
This definition is referenced by: isnlly 22071 nllyeq 22073 |
Copyright terms: Public domain | W3C validator |