![]() |
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 23489 | . 2 class 𝑛-Locally 𝐴 |
3 | vj | . . . . . . . . 9 setvar 𝑗 | |
4 | 3 | cv 1536 | . . . . . . . 8 class 𝑗 |
5 | vu | . . . . . . . . 9 setvar 𝑢 | |
6 | 5 | cv 1536 | . . . . . . . 8 class 𝑢 |
7 | crest 17467 | . . . . . . . 8 class ↾t | |
8 | 4, 6, 7 | co 7431 | . . . . . . 7 class (𝑗 ↾t 𝑢) |
9 | 8, 1 | wcel 2106 | . . . . . 6 wff (𝑗 ↾t 𝑢) ∈ 𝐴 |
10 | vy | . . . . . . . . . 10 setvar 𝑦 | |
11 | 10 | cv 1536 | . . . . . . . . 9 class 𝑦 |
12 | 11 | csn 4631 | . . . . . . . 8 class {𝑦} |
13 | cnei 23121 | . . . . . . . . 9 class nei | |
14 | 4, 13 | cfv 6563 | . . . . . . . 8 class (nei‘𝑗) |
15 | 12, 14 | cfv 6563 | . . . . . . 7 class ((nei‘𝑗)‘{𝑦}) |
16 | vx | . . . . . . . . 9 setvar 𝑥 | |
17 | 16 | cv 1536 | . . . . . . . 8 class 𝑥 |
18 | 17 | cpw 4605 | . . . . . . 7 class 𝒫 𝑥 |
19 | 15, 18 | cin 3962 | . . . . . 6 class (((nei‘𝑗)‘{𝑦}) ∩ 𝒫 𝑥) |
20 | 9, 5, 19 | wrex 3068 | . . . . 5 wff ∃𝑢 ∈ (((nei‘𝑗)‘{𝑦}) ∩ 𝒫 𝑥)(𝑗 ↾t 𝑢) ∈ 𝐴 |
21 | 20, 10, 17 | wral 3059 | . . . 4 wff ∀𝑦 ∈ 𝑥 ∃𝑢 ∈ (((nei‘𝑗)‘{𝑦}) ∩ 𝒫 𝑥)(𝑗 ↾t 𝑢) ∈ 𝐴 |
22 | 21, 16, 4 | wral 3059 | . . 3 wff ∀𝑥 ∈ 𝑗 ∀𝑦 ∈ 𝑥 ∃𝑢 ∈ (((nei‘𝑗)‘{𝑦}) ∩ 𝒫 𝑥)(𝑗 ↾t 𝑢) ∈ 𝐴 |
23 | ctop 22915 | . . 3 class Top | |
24 | 22, 3, 23 | crab 3433 | . 2 class {𝑗 ∈ Top ∣ ∀𝑥 ∈ 𝑗 ∀𝑦 ∈ 𝑥 ∃𝑢 ∈ (((nei‘𝑗)‘{𝑦}) ∩ 𝒫 𝑥)(𝑗 ↾t 𝑢) ∈ 𝐴} |
25 | 2, 24 | wceq 1537 | 1 wff 𝑛-Locally 𝐴 = {𝑗 ∈ Top ∣ ∀𝑥 ∈ 𝑗 ∀𝑦 ∈ 𝑥 ∃𝑢 ∈ (((nei‘𝑗)‘{𝑦}) ∩ 𝒫 𝑥)(𝑗 ↾t 𝑢) ∈ 𝐴} |
Colors of variables: wff setvar class |
This definition is referenced by: isnlly 23493 nllyeq 23495 |
Copyright terms: Public domain | W3C validator |