Metamath Proof Explorer

Definition df-nlly

Description: Define a space that is n-locally A , where A is a topological property like "compact", "connected", or "path-connected". A topological space is n-locally A if every neighborhood of a point contains a subneighborhood that is A in the subspace topology.

The terminology "n-locally", where 'n' stands for "neighborhood", is not standard, although this is sometimes called "weakly locally A ". The reason for the distinction is that some notions only make sense for arbitrary neighborhoods (such as "locally compact", which is actually N-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
Assertion df-nlly ⊢ N-Locally A = j ∈ Top | ∀ x ∈ j ∀ y ∈ x ∃ u ∈ nei ⁡ j ⁡ y ∩ 𝒫 x j ↾ 𝑡 u ∈ A

Detailed syntax breakdown

Step Hyp Ref Expression
0 cA class A
1 0 cnlly class N-Locally A
2 vj setvar j
3 ctop class Top
4 vx setvar x
5 2 cv setvar j
6 vy setvar y
7 4 cv setvar x
8 vu setvar u
9 cnei class nei
10 5 9 cfv class nei ⁡ j
11 6 cv setvar y
12 11 csn class y
13 12 10 cfv class nei ⁡ j ⁡ y
14 7 cpw class 𝒫 x
15 13 14 cin class nei ⁡ j ⁡ y ∩ 𝒫 x
16 crest class ↾ 𝑡
17 8 cv setvar u
18 5 17 16 co class j ↾ 𝑡 u
19 18 0 wcel wff j ↾ 𝑡 u ∈ A
20 19 8 15 wrex wff ∃ u ∈ nei ⁡ j ⁡ y ∩ 𝒫 x j ↾ 𝑡 u ∈ A
21 20 6 7 wral wff ∀ y ∈ x ∃ u ∈ nei ⁡ j ⁡ y ∩ 𝒫 x j ↾ 𝑡 u ∈ A
22 21 4 5 wral wff ∀ x ∈ j ∀ y ∈ x ∃ u ∈ nei ⁡ j ⁡ y ∩ 𝒫 x j ↾ 𝑡 u ∈ A
23 22 2 3 crab class j ∈ Top | ∀ x ∈ j ∀ y ∈ x ∃ u ∈ nei ⁡ j ⁡ y ∩ 𝒫 x j ↾ 𝑡 u ∈ A
24 1 23 wceq wff N-Locally A = j ∈ Top | ∀ x ∈ j ∀ y ∈ x ∃ u ∈ nei ⁡ j ⁡ y ∩ 𝒫 x j ↾ 𝑡 u ∈ A