Skip to content

Commit cfa9570

Browse files
lowasserlowasser
authored
Every point in a proper closed interval in the real numbers is an accumulation point (#1679)
...and the definition of what an accumulation point _is_, and so on. This is intended as a key step to #1615; let me sketch it out. Let `f` be a function from `[a,b]` to the real numbers, where `a < b`. The derivative of a function at a point is -- well, defined another way, but we can show that given a sequence `y` approaching `x` but remaining apart from it, the derivative at `x` is equal to the unique limit of (f y - f x)/(y - x) as y approaches x. Such a sequence exists if and only if x is an accumulation point of the space where the function is defined. This PR proves every point in a proper closed interval is an accumulation point, so the value of any derivative of `f` at `x` is unique, so all derivatives are homotopic, so derivatives are unique and being differentiable is a proposition.
1 parent de15078 commit cfa9570

19 files changed

+1180
-5
lines changed

‎src/elementary-number-theory/addition-positive-rational-numbers.lagda.md‎

Lines changed: 5 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -453,11 +453,12 @@ module _
453453
( left-summand-split-ℚ⁺ p)
454454
( right-summand-split-ℚ⁺ p))
455455
456-
bound-double-le-ℚ⁺ :
457-
Σ ℚ⁺ (λ q → le-ℚ⁺ (q +ℚ⁺ q) p)
458-
bound-double-le-ℚ⁺ =
459-
( modulus-le-double-le-ℚ⁺ , le-double-le-modulus-le-double-le-ℚ⁺)
456+
bound-double-le-ℚ⁺ :
457+
Σ ℚ⁺ (λ q → le-ℚ⁺ (q +ℚ⁺ q) p)
458+
bound-double-le-ℚ⁺ =
459+
( modulus-le-double-le-ℚ⁺ , le-double-le-modulus-le-double-le-ℚ⁺)
460460
461+
abstract
461462
double-le-ℚ⁺ : exists ℚ⁺ (λ q → le-prop-ℚ⁺ (q +ℚ⁺ q) p)
462463
double-le-ℚ⁺ = unit-trunc-Prop bound-double-le-ℚ⁺
463464
```

‎src/metric-spaces.lagda.md‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -56,6 +56,7 @@ metric space, `N d₂ x y` [or](foundation.disjunction.md)
5656
```agda
5757
module metric-spaces where
5858
59+
open import metric-spaces.accumulation-points-subsets-located-metric-spaces public
5960
open import metric-spaces.apartness-located-metric-spaces public
6061
open import metric-spaces.approximations-located-metric-spaces public
6162
open import metric-spaces.approximations-metric-spaces public

‎src/metric-spaces/accumulation-points-subsets-located-metric-spaces.lagda.md‎

Lines changed: 319 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,319 @@
1+
# Accumulation points of subsets of located metric spaces
2+
3+
```agda
4+
module metric-spaces.accumulation-points-subsets-located-metric-spaces where
5+
```
6+
7+
<details><summary>Imports</summary>
8+
9+
```agda
10+
open import elementary-number-theory.addition-positive-rational-numbers
11+
open import elementary-number-theory.inequality-natural-numbers
12+
open import elementary-number-theory.natural-numbers
13+
open import elementary-number-theory.positive-rational-numbers
14+
open import elementary-number-theory.strict-inequality-rational-numbers
15+
16+
open import foundation.conjunction
17+
open import foundation.dependent-pair-types
18+
open import foundation.existential-quantification
19+
open import foundation.function-types
20+
open import foundation.intersections-subtypes
21+
open import foundation.logical-equivalences
22+
open import foundation.propositional-truncations
23+
open import foundation.propositions
24+
open import foundation.subtypes
25+
open import foundation.universe-levels
26+
27+
open import lists.sequences
28+
29+
open import logic.functoriality-existential-quantification
30+
31+
open import metric-spaces.apartness-located-metric-spaces
32+
open import metric-spaces.cauchy-approximations-metric-spaces
33+
open import metric-spaces.cauchy-sequences-metric-spaces
34+
open import metric-spaces.closed-subsets-located-metric-spaces
35+
open import metric-spaces.limits-of-cauchy-approximations-metric-spaces
36+
open import metric-spaces.limits-of-sequences-metric-spaces
37+
open import metric-spaces.located-metric-spaces
38+
open import metric-spaces.subspaces-metric-spaces
39+
```
40+
41+
</details>
42+
43+
## Idea
44+
45+
An
46+
{{#concept "accumulation point" WDID=Q858223 WD="limit point" Disambiguation="of a subset of a located metric space" Agda=accumulation-point-subset-Located-Metric-Space}}
47+
of a subset `S` of a
48+
[located metric space](metric-spaces.located-metric-spaces.md) `X` is a point
49+
`x : X` such that there exists a
50+
[Cauchy approximation](metric-spaces.cauchy-approximations-metric-spaces.md) `a`
51+
with [limit](metric-spaces.limits-of-cauchy-approximations-metric-spaces.md) `x`
52+
such that for every `ε : ℚ⁺`, `a ε` is in `S` and is
53+
[apart](metric-spaces.apartness-located-metric-spaces.md) from `x`. In
54+
particular, this implies an accumulation point is not isolated.
55+
56+
## Definition
57+
58+
```agda
59+
module _
60+
{l1 l2 l3 : Level}
61+
(X : Located-Metric-Space l1 l2)
62+
(S : subset-Located-Metric-Space l3 X)
63+
where
64+
65+
is-accumulation-to-point-prop-subset-Located-Metric-Space :
66+
type-Located-Metric-Space X →
67+
subtype
68+
( l2)
69+
( cauchy-approximation-Metric-Space (subspace-Located-Metric-Space X S))
70+
is-accumulation-to-point-prop-subset-Located-Metric-Space x a =
71+
Π-Prop
72+
( ℚ⁺)
73+
( λ ε →
74+
apart-prop-Located-Metric-Space X
75+
( pr1
76+
( map-cauchy-approximation-Metric-Space
77+
( subspace-Located-Metric-Space X S)
78+
( a)
79+
( ε)))
80+
( x)) ∧
81+
is-limit-cauchy-approximation-prop-Metric-Space
82+
( metric-space-Located-Metric-Space X)
83+
( map-short-function-cauchy-approximation-Metric-Space
84+
( subspace-Located-Metric-Space X S)
85+
( metric-space-Located-Metric-Space X)
86+
( short-inclusion-subspace-Metric-Space
87+
( metric-space-Located-Metric-Space X)
88+
( S))
89+
( a))
90+
( x)
91+
92+
is-accumulation-to-point-subset-Located-Metric-Space :
93+
type-Located-Metric-Space X →
94+
cauchy-approximation-Metric-Space (subspace-Located-Metric-Space X S) →
95+
UU l2
96+
is-accumulation-to-point-subset-Located-Metric-Space x a =
97+
type-Prop (is-accumulation-to-point-prop-subset-Located-Metric-Space x a)
98+
99+
is-accumulation-point-prop-subset-Located-Metric-Space :
100+
subset-Metric-Space (l1 ⊔ l2 ⊔ l3) (metric-space-Located-Metric-Space X)
101+
is-accumulation-point-prop-subset-Located-Metric-Space x =
102+
∃ ( cauchy-approximation-Metric-Space (subspace-Located-Metric-Space X S))
103+
( is-accumulation-to-point-prop-subset-Located-Metric-Space x)
104+
105+
is-accumulation-point-subset-Located-Metric-Space :
106+
type-Located-Metric-Space X → UU (l1 ⊔ l2 ⊔ l3)
107+
is-accumulation-point-subset-Located-Metric-Space x =
108+
type-Prop (is-accumulation-point-prop-subset-Located-Metric-Space x)
109+
110+
accumulation-point-subset-Located-Metric-Space : UU (l1 ⊔ l2 ⊔ l3)
111+
accumulation-point-subset-Located-Metric-Space =
112+
type-subtype is-accumulation-point-prop-subset-Located-Metric-Space
113+
```
114+
115+
## Properties
116+
117+
### A closed subset of a metric space contains all its accumulation points
118+
119+
```agda
120+
module _
121+
{l1 l2 l3 : Level}
122+
(X : Located-Metric-Space l1 l2)
123+
(S : closed-subset-Located-Metric-Space l3 X)
124+
where
125+
126+
is-in-closed-subset-is-accumulation-point-Located-Metric-Space :
127+
(x : type-Located-Metric-Space X) →
128+
is-accumulation-point-subset-Located-Metric-Space
129+
( X)
130+
( subset-closed-subset-Located-Metric-Space X S)
131+
( x) →
132+
is-in-closed-subset-Located-Metric-Space X S x
133+
is-in-closed-subset-is-accumulation-point-Located-Metric-Space x is-acc-x =
134+
is-closed-subset-closed-subset-Located-Metric-Space
135+
( X)
136+
( S)
137+
( x)
138+
( λ ε →
139+
let
140+
open
141+
do-syntax-trunc-Prop
142+
( ∃
143+
( type-Located-Metric-Space X)
144+
( λ y →
145+
neighborhood-prop-Located-Metric-Space X ε x y ∧
146+
subset-closed-subset-Located-Metric-Space X S y))
147+
in do
148+
(approx@(a , _) , a#x , lim-a=x) ← is-acc-x
149+
let (y , y∈S) = a ε
150+
intro-exists
151+
( y)
152+
( symmetric-neighborhood-Located-Metric-Space X
153+
( ε)
154+
( y)
155+
( x)
156+
( saturated-is-limit-cauchy-approximation-Metric-Space
157+
( metric-space-Located-Metric-Space X)
158+
( map-short-function-cauchy-approximation-Metric-Space
159+
( subspace-Located-Metric-Space
160+
( X)
161+
( subset-closed-subset-Located-Metric-Space X S))
162+
( metric-space-Located-Metric-Space X)
163+
( short-inclusion-subspace-Metric-Space
164+
( metric-space-Located-Metric-Space X)
165+
( subset-closed-subset-Located-Metric-Space X S))
166+
( approx))
167+
( x)
168+
( lim-a=x)
169+
( ε)) ,
170+
y∈S))
171+
```
172+
173+
### The property of being a sequential accumulation point
174+
175+
```agda
176+
module _
177+
{l1 l2 l3 : Level}
178+
(X : Located-Metric-Space l1 l2)
179+
(S : subset-Located-Metric-Space l3 X)
180+
(x : type-Located-Metric-Space X)
181+
where
182+
183+
is-sequence-accumulating-to-point-prop-subset-Located-Metric-Space :
184+
subtype l2 (sequence (type-subtype S))
185+
is-sequence-accumulating-to-point-prop-subset-Located-Metric-Space a =
186+
Π-Prop ℕ (λ n → apart-prop-Located-Metric-Space X (pr1 (a n)) x) ∧
187+
is-limit-prop-sequence-Metric-Space
188+
( metric-space-Located-Metric-Space X)
189+
( pr1 ∘ a)
190+
( x)
191+
192+
is-sequence-accumulating-to-point-subset-Located-Metric-Space :
193+
sequence (type-subtype S) → UU l2
194+
is-sequence-accumulating-to-point-subset-Located-Metric-Space =
195+
is-in-subtype
196+
( is-sequence-accumulating-to-point-prop-subset-Located-Metric-Space)
197+
198+
is-sequential-accumulation-point-prop-subset-Located-Metric-Space :
199+
Prop (l1 ⊔ l2 ⊔ l3)
200+
is-sequential-accumulation-point-prop-subset-Located-Metric-Space =
201+
∃ ( sequence (type-subtype S))
202+
( is-sequence-accumulating-to-point-prop-subset-Located-Metric-Space)
203+
204+
is-sequential-accumulation-point-subset-Located-Metric-Space :
205+
UU (l1 ⊔ l2 ⊔ l3)
206+
is-sequential-accumulation-point-subset-Located-Metric-Space =
207+
type-Prop is-sequential-accumulation-point-prop-subset-Located-Metric-Space
208+
```
209+
210+
### If `x` is an accumulation point of `S`, it is a sequential accumulation point of `S`
211+
212+
```agda
213+
module _
214+
{l1 l2 l3 : Level}
215+
(X : Located-Metric-Space l1 l2)
216+
(S : subset-Located-Metric-Space l3 X)
217+
(x : type-Located-Metric-Space X)
218+
where
219+
220+
abstract
221+
is-sequential-accumulation-point-is-accumulation-point-subset-Located-Metric-Space :
222+
is-accumulation-point-subset-Located-Metric-Space X S x →
223+
is-sequential-accumulation-point-subset-Located-Metric-Space X S x
224+
is-sequential-accumulation-point-is-accumulation-point-subset-Located-Metric-Space =
225+
map-exists
226+
( _)
227+
( map-cauchy-sequence-cauchy-approximation-Metric-Space
228+
( subspace-Located-Metric-Space X S))
229+
( λ a (a#x , lim-a=x) →
230+
( ( λ n → a#x _) ,
231+
is-limit-cauchy-sequence-cauchy-approximation-Metric-Space
232+
( metric-space-Located-Metric-Space X)
233+
( map-short-function-cauchy-approximation-Metric-Space
234+
( subspace-Located-Metric-Space X S)
235+
( metric-space-Located-Metric-Space X)
236+
( short-inclusion-subspace-Metric-Space
237+
( metric-space-Located-Metric-Space X)
238+
( S))
239+
( a))
240+
( x)
241+
( lim-a=x)))
242+
```
243+
244+
### If `x` is a sequential accumulation point of `S`, it is an accumulation point of `S`
245+
246+
```agda
247+
module _
248+
{l1 l2 l3 : Level}
249+
(X : Located-Metric-Space l1 l2)
250+
(S : subset-Located-Metric-Space l3 X)
251+
(x : type-Located-Metric-Space X)
252+
where
253+
254+
abstract
255+
is-accumulation-point-is-sequential-accumulation-point-subset-Located-Metric-Space :
256+
is-sequential-accumulation-point-subset-Located-Metric-Space X S x →
257+
is-accumulation-point-subset-Located-Metric-Space X S x
258+
is-accumulation-point-is-sequential-accumulation-point-subset-Located-Metric-Space
259+
is-seq-acc-x =
260+
let
261+
open
262+
do-syntax-trunc-Prop
263+
( is-accumulation-point-prop-subset-Located-Metric-Space X S x)
264+
in do
265+
(σ , σ#x , lim-σ=x) ← is-seq-acc-x
266+
μ@(mod-μ , is-mod-μ) ← lim-σ=x
267+
intro-exists
268+
( cauchy-approximation-cauchy-sequence-Metric-Space
269+
( subspace-Located-Metric-Space X S)
270+
( σ ,
271+
is-cauchy-has-limit-modulus-sequence-Metric-Space
272+
( metric-space-Located-Metric-Space X)
273+
( pr1 ∘ σ)
274+
( x)
275+
( μ)))
276+
( ( λ ε → σ#x _) ,
277+
( λ ε δ →
278+
let ε' = modulus-le-double-le-ℚ⁺ ε
279+
in
280+
monotonic-neighborhood-Located-Metric-Space
281+
( X)
282+
( pr1 (σ (mod-μ ε')))
283+
( x)
284+
( ε')
285+
( ε +ℚ⁺ δ)
286+
( transitive-le-ℚ _ _ _
287+
( le-left-add-ℚ⁺ ε δ)
288+
( le-modulus-le-double-le-ℚ⁺ ε))
289+
( is-mod-μ ε' (mod-μ ε') (refl-leq-ℕ (mod-μ ε')))))
290+
```
291+
292+
### Being an accumulation point is equivalent to being a sequential accumulation point
293+
294+
```agda
295+
module _
296+
{l1 l2 l3 : Level}
297+
(X : Located-Metric-Space l1 l2)
298+
(S : subset-Located-Metric-Space l3 X)
299+
(x : type-Located-Metric-Space X)
300+
where
301+
302+
is-accumulation-point-iff-is-sequential-accumulation-point-subset-Located-Metric-Space :
303+
is-accumulation-point-subset-Located-Metric-Space X S x ↔
304+
is-sequential-accumulation-point-subset-Located-Metric-Space X S x
305+
is-accumulation-point-iff-is-sequential-accumulation-point-subset-Located-Metric-Space =
306+
( is-sequential-accumulation-point-is-accumulation-point-subset-Located-Metric-Space
307+
( X)
308+
( S)
309+
( x) ,
310+
is-accumulation-point-is-sequential-accumulation-point-subset-Located-Metric-Space
311+
( X)
312+
( S)
313+
( x))
314+
```
315+
316+
## External links
317+
318+
- [Accumulation point](https://en.wikipedia.org/wiki/Accumulation_point) on
319+
Wikipedia

0 commit comments

Comments
 (0)