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 22001 | . 2 class 𝑛-Locally 𝐴 |
3 | vj | . . . . . . . . 9 setvar 𝑗 | |
4 | 3 | cv 1527 | . . . . . . . 8 class 𝑗 |
5 | vu | . . . . . . . . 9 setvar 𝑢 | |
6 | 5 | cv 1527 | . . . . . . . 8 class 𝑢 |
7 | crest 16682 | . . . . . . . 8 class ↾t | |
8 | 4, 6, 7 | co 7145 | . . . . . . 7 class (𝑗 ↾t 𝑢) |
9 | 8, 1 | wcel 2105 | . . . . . 6 wff (𝑗 ↾t 𝑢) ∈ 𝐴 |
10 | vy | . . . . . . . . . 10 setvar 𝑦 | |
11 | 10 | cv 1527 | . . . . . . . . 9 class 𝑦 |
12 | 11 | csn 4557 | . . . . . . . 8 class {𝑦} |
13 | cnei 21633 | . . . . . . . . 9 class nei | |
14 | 4, 13 | cfv 6348 | . . . . . . . 8 class (nei‘𝑗) |
15 | 12, 14 | cfv 6348 | . . . . . . 7 class ((nei‘𝑗)‘{𝑦}) |
16 | vx | . . . . . . . . 9 setvar 𝑥 | |
17 | 16 | cv 1527 | . . . . . . . 8 class 𝑥 |
18 | 17 | cpw 4535 | . . . . . . 7 class 𝒫 𝑥 |
19 | 15, 18 | cin 3932 | . . . . . 6 class (((nei‘𝑗)‘{𝑦}) ∩ 𝒫 𝑥) |
20 | 9, 5, 19 | wrex 3136 | . . . . 5 wff ∃𝑢 ∈ (((nei‘𝑗)‘{𝑦}) ∩ 𝒫 𝑥)(𝑗 ↾t 𝑢) ∈ 𝐴 |
21 | 20, 10, 17 | wral 3135 | . . . 4 wff ∀𝑦 ∈ 𝑥 ∃𝑢 ∈ (((nei‘𝑗)‘{𝑦}) ∩ 𝒫 𝑥)(𝑗 ↾t 𝑢) ∈ 𝐴 |
22 | 21, 16, 4 | wral 3135 | . . 3 wff ∀𝑥 ∈ 𝑗 ∀𝑦 ∈ 𝑥 ∃𝑢 ∈ (((nei‘𝑗)‘{𝑦}) ∩ 𝒫 𝑥)(𝑗 ↾t 𝑢) ∈ 𝐴 |
23 | ctop 21429 | . . 3 class Top | |
24 | 22, 3, 23 | crab 3139 | . 2 class {𝑗 ∈ Top ∣ ∀𝑥 ∈ 𝑗 ∀𝑦 ∈ 𝑥 ∃𝑢 ∈ (((nei‘𝑗)‘{𝑦}) ∩ 𝒫 𝑥)(𝑗 ↾t 𝑢) ∈ 𝐴} |
25 | 2, 24 | wceq 1528 | 1 wff 𝑛-Locally 𝐴 = {𝑗 ∈ Top ∣ ∀𝑥 ∈ 𝑗 ∀𝑦 ∈ 𝑥 ∃𝑢 ∈ (((nei‘𝑗)‘{𝑦}) ∩ 𝒫 𝑥)(𝑗 ↾t 𝑢) ∈ 𝐴} |
Colors of variables: wff setvar class |
This definition is referenced by: isnlly 22005 nllyeq 22007 |
Copyright terms: Public domain | W3C validator |