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 23291
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 23289 . 2 class 𝑛-Locally 𝐴
3 vj . . . . . . . . 9 setvar 𝑗
43cv 1539 . . . . . . . 8 class 𝑗
5 vu . . . . . . . . 9 setvar 𝑒
65cv 1539 . . . . . . . 8 class 𝑒
7 crest 17373 . . . . . . . 8 class β†Ύt
84, 6, 7co 7412 . . . . . . 7 class (𝑗 β†Ύt 𝑒)
98, 1wcel 2105 . . . . . 6 wff (𝑗 β†Ύt 𝑒) ∈ 𝐴
10 vy . . . . . . . . . 10 setvar 𝑦
1110cv 1539 . . . . . . . . 9 class 𝑦
1211csn 4628 . . . . . . . 8 class {𝑦}
13 cnei 22921 . . . . . . . . 9 class nei
144, 13cfv 6543 . . . . . . . 8 class (neiβ€˜π‘—)
1512, 14cfv 6543 . . . . . . 7 class ((neiβ€˜π‘—)β€˜{𝑦})
16 vx . . . . . . . . 9 setvar π‘₯
1716cv 1539 . . . . . . . 8 class π‘₯
1817cpw 4602 . . . . . . 7 class 𝒫 π‘₯
1915, 18cin 3947 . . . . . 6 class (((neiβ€˜π‘—)β€˜{𝑦}) ∩ 𝒫 π‘₯)
209, 5, 19wrex 3069 . . . . 5 wff βˆƒπ‘’ ∈ (((neiβ€˜π‘—)β€˜{𝑦}) ∩ 𝒫 π‘₯)(𝑗 β†Ύt 𝑒) ∈ 𝐴
2120, 10, 17wral 3060 . . . 4 wff βˆ€π‘¦ ∈ π‘₯ βˆƒπ‘’ ∈ (((neiβ€˜π‘—)β€˜{𝑦}) ∩ 𝒫 π‘₯)(𝑗 β†Ύt 𝑒) ∈ 𝐴
2221, 16, 4wral 3060 . . 3 wff βˆ€π‘₯ ∈ 𝑗 βˆ€π‘¦ ∈ π‘₯ βˆƒπ‘’ ∈ (((neiβ€˜π‘—)β€˜{𝑦}) ∩ 𝒫 π‘₯)(𝑗 β†Ύt 𝑒) ∈ 𝐴
23 ctop 22715 . . 3 class Top
2422, 3, 23crab 3431 . 2 class {𝑗 ∈ Top ∣ βˆ€π‘₯ ∈ 𝑗 βˆ€π‘¦ ∈ π‘₯ βˆƒπ‘’ ∈ (((neiβ€˜π‘—)β€˜{𝑦}) ∩ 𝒫 π‘₯)(𝑗 β†Ύt 𝑒) ∈ 𝐴}
252, 24wceq 1540 1 wff 𝑛-Locally 𝐴 = {𝑗 ∈ Top ∣ βˆ€π‘₯ ∈ 𝑗 βˆ€π‘¦ ∈ π‘₯ βˆƒπ‘’ ∈ (((neiβ€˜π‘—)β€˜{𝑦}) ∩ 𝒫 π‘₯)(𝑗 β†Ύt 𝑒) ∈ 𝐴}
Colors of variables: wff setvar class
This definition is referenced by:  isnlly  23293  nllyeq  23295
  Copyright terms: Public domain W3C validator