| 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 23473 | . 2 class 𝑛-Locally 𝐴 |
| 3 | vj | . . . . . . . . 9 setvar 𝑗 | |
| 4 | 3 | cv 1539 | . . . . . . . 8 class 𝑗 |
| 5 | vu | . . . . . . . . 9 setvar 𝑢 | |
| 6 | 5 | cv 1539 | . . . . . . . 8 class 𝑢 |
| 7 | crest 17465 | . . . . . . . 8 class ↾t | |
| 8 | 4, 6, 7 | co 7431 | . . . . . . 7 class (𝑗 ↾t 𝑢) |
| 9 | 8, 1 | wcel 2108 | . . . . . 6 wff (𝑗 ↾t 𝑢) ∈ 𝐴 |
| 10 | vy | . . . . . . . . . 10 setvar 𝑦 | |
| 11 | 10 | cv 1539 | . . . . . . . . 9 class 𝑦 |
| 12 | 11 | csn 4626 | . . . . . . . 8 class {𝑦} |
| 13 | cnei 23105 | . . . . . . . . 9 class nei | |
| 14 | 4, 13 | cfv 6561 | . . . . . . . 8 class (nei‘𝑗) |
| 15 | 12, 14 | cfv 6561 | . . . . . . 7 class ((nei‘𝑗)‘{𝑦}) |
| 16 | vx | . . . . . . . . 9 setvar 𝑥 | |
| 17 | 16 | cv 1539 | . . . . . . . 8 class 𝑥 |
| 18 | 17 | cpw 4600 | . . . . . . 7 class 𝒫 𝑥 |
| 19 | 15, 18 | cin 3950 | . . . . . 6 class (((nei‘𝑗)‘{𝑦}) ∩ 𝒫 𝑥) |
| 20 | 9, 5, 19 | wrex 3070 | . . . . 5 wff ∃𝑢 ∈ (((nei‘𝑗)‘{𝑦}) ∩ 𝒫 𝑥)(𝑗 ↾t 𝑢) ∈ 𝐴 |
| 21 | 20, 10, 17 | wral 3061 | . . . 4 wff ∀𝑦 ∈ 𝑥 ∃𝑢 ∈ (((nei‘𝑗)‘{𝑦}) ∩ 𝒫 𝑥)(𝑗 ↾t 𝑢) ∈ 𝐴 |
| 22 | 21, 16, 4 | wral 3061 | . . 3 wff ∀𝑥 ∈ 𝑗 ∀𝑦 ∈ 𝑥 ∃𝑢 ∈ (((nei‘𝑗)‘{𝑦}) ∩ 𝒫 𝑥)(𝑗 ↾t 𝑢) ∈ 𝐴 |
| 23 | ctop 22899 | . . 3 class Top | |
| 24 | 22, 3, 23 | crab 3436 | . 2 class {𝑗 ∈ Top ∣ ∀𝑥 ∈ 𝑗 ∀𝑦 ∈ 𝑥 ∃𝑢 ∈ (((nei‘𝑗)‘{𝑦}) ∩ 𝒫 𝑥)(𝑗 ↾t 𝑢) ∈ 𝐴} |
| 25 | 2, 24 | wceq 1540 | 1 wff 𝑛-Locally 𝐴 = {𝑗 ∈ Top ∣ ∀𝑥 ∈ 𝑗 ∀𝑦 ∈ 𝑥 ∃𝑢 ∈ (((nei‘𝑗)‘{𝑦}) ∩ 𝒫 𝑥)(𝑗 ↾t 𝑢) ∈ 𝐴} |
| Colors of variables: wff setvar class |
| This definition is referenced by: isnlly 23477 nllyeq 23479 |
| Copyright terms: Public domain | W3C validator |