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

Definition df-nlly 21080
 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 sub-neighborhood 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 21078 . 2 class 𝑛-Locally 𝐴
3 vj . . . . . . . . 9 setvar 𝑗
43cv 1474 . . . . . . . 8 class 𝑗
5 vu . . . . . . . . 9 setvar 𝑢
65cv 1474 . . . . . . . 8 class 𝑢
7 crest 15904 . . . . . . . 8 class t
84, 6, 7co 6549 . . . . . . 7 class (𝑗t 𝑢)
98, 1wcel 1977 . . . . . 6 wff (𝑗t 𝑢) ∈ 𝐴
10 vy . . . . . . . . . 10 setvar 𝑦
1110cv 1474 . . . . . . . . 9 class 𝑦
1211csn 4125 . . . . . . . 8 class {𝑦}
13 cnei 20711 . . . . . . . . 9 class nei
144, 13cfv 5804 . . . . . . . 8 class (nei‘𝑗)
1512, 14cfv 5804 . . . . . . 7 class ((nei‘𝑗)‘{𝑦})
16 vx . . . . . . . . 9 setvar 𝑥
1716cv 1474 . . . . . . . 8 class 𝑥
1817cpw 4108 . . . . . . 7 class 𝒫 𝑥
1915, 18cin 3539 . . . . . 6 class (((nei‘𝑗)‘{𝑦}) ∩ 𝒫 𝑥)
209, 5, 19wrex 2897 . . . . 5 wff 𝑢 ∈ (((nei‘𝑗)‘{𝑦}) ∩ 𝒫 𝑥)(𝑗t 𝑢) ∈ 𝐴
2120, 10, 17wral 2896 . . . 4 wff 𝑦𝑥𝑢 ∈ (((nei‘𝑗)‘{𝑦}) ∩ 𝒫 𝑥)(𝑗t 𝑢) ∈ 𝐴
2221, 16, 4wral 2896 . . 3 wff 𝑥𝑗𝑦𝑥𝑢 ∈ (((nei‘𝑗)‘{𝑦}) ∩ 𝒫 𝑥)(𝑗t 𝑢) ∈ 𝐴
23 ctop 20517 . . 3 class Top
2422, 3, 23crab 2900 . 2 class {𝑗 ∈ Top ∣ ∀𝑥𝑗𝑦𝑥𝑢 ∈ (((nei‘𝑗)‘{𝑦}) ∩ 𝒫 𝑥)(𝑗t 𝑢) ∈ 𝐴}
252, 24wceq 1475 1 wff 𝑛-Locally 𝐴 = {𝑗 ∈ Top ∣ ∀𝑥𝑗𝑦𝑥𝑢 ∈ (((nei‘𝑗)‘{𝑦}) ∩ 𝒫 𝑥)(𝑗t 𝑢) ∈ 𝐴}
 Colors of variables: wff setvar class This definition is referenced by:  isnlly  21082  nllyeq  21084
 Copyright terms: Public domain W3C validator