MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-nlly Structured version   Visualization version   GIF version

Definition df-nlly 22940
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.)

Assertion
Ref Expression
df-nlly 𝑛-Locally 𝐴 = {𝑗 ∈ Top ∣ ∀𝑥𝑗𝑦𝑥𝑢 ∈ (((nei‘𝑗)‘{𝑦}) ∩ 𝒫 𝑥)(𝑗t 𝑢) ∈ 𝐴}
Distinct variable group:   𝑢,𝑗,𝑥,𝑦,𝐴

Detailed syntax breakdown of Definition df-nlly
StepHypRef Expression
1 cA . . 3 class 𝐴
21cnlly 22938 . 2 class 𝑛-Locally 𝐴
3 vj . . . . . . . . 9 setvar 𝑗
43cv 1541 . . . . . . . 8 class 𝑗
5 vu . . . . . . . . 9 setvar 𝑢
65cv 1541 . . . . . . . 8 class 𝑢
7 crest 17353 . . . . . . . 8 class t
84, 6, 7co 7396 . . . . . . 7 class (𝑗t 𝑢)
98, 1wcel 2107 . . . . . 6 wff (𝑗t 𝑢) ∈ 𝐴
10 vy . . . . . . . . . 10 setvar 𝑦
1110cv 1541 . . . . . . . . 9 class 𝑦
1211csn 4624 . . . . . . . 8 class {𝑦}
13 cnei 22570 . . . . . . . . 9 class nei
144, 13cfv 6535 . . . . . . . 8 class (nei‘𝑗)
1512, 14cfv 6535 . . . . . . 7 class ((nei‘𝑗)‘{𝑦})
16 vx . . . . . . . . 9 setvar 𝑥
1716cv 1541 . . . . . . . 8 class 𝑥
1817cpw 4598 . . . . . . 7 class 𝒫 𝑥
1915, 18cin 3945 . . . . . 6 class (((nei‘𝑗)‘{𝑦}) ∩ 𝒫 𝑥)
209, 5, 19wrex 3071 . . . . 5 wff 𝑢 ∈ (((nei‘𝑗)‘{𝑦}) ∩ 𝒫 𝑥)(𝑗t 𝑢) ∈ 𝐴
2120, 10, 17wral 3062 . . . 4 wff 𝑦𝑥𝑢 ∈ (((nei‘𝑗)‘{𝑦}) ∩ 𝒫 𝑥)(𝑗t 𝑢) ∈ 𝐴
2221, 16, 4wral 3062 . . 3 wff 𝑥𝑗𝑦𝑥𝑢 ∈ (((nei‘𝑗)‘{𝑦}) ∩ 𝒫 𝑥)(𝑗t 𝑢) ∈ 𝐴
23 ctop 22364 . . 3 class Top
2422, 3, 23crab 3433 . 2 class {𝑗 ∈ Top ∣ ∀𝑥𝑗𝑦𝑥𝑢 ∈ (((nei‘𝑗)‘{𝑦}) ∩ 𝒫 𝑥)(𝑗t 𝑢) ∈ 𝐴}
252, 24wceq 1542 1 wff 𝑛-Locally 𝐴 = {𝑗 ∈ Top ∣ ∀𝑥𝑗𝑦𝑥𝑢 ∈ (((nei‘𝑗)‘{𝑦}) ∩ 𝒫 𝑥)(𝑗t 𝑢) ∈ 𝐴}
Colors of variables: wff setvar class
This definition is referenced by:  isnlly  22942  nllyeq  22944
  Copyright terms: Public domain W3C validator