Proof of Nuprl Lemma : interval-fun-maps-compact

Step * 1 1 1 of Lemma interval-fun-maps-compact

.....assertion.....
1. J : Interval
2. n : ℕ⁺
3. a : ℝ
4. b : ℝ
5. a ≤ b
6. g : [a, b] ⟶ℝ
7. interval-fun([a, b];J;x.g[x])
8. real-fun(g;a;b)
9. ∀c:ℝ. ((∀x:{x:ℝ| x ∈ [a, b]} . (c < (g x))) ⇒ (∃c':{c':ℝ| c < c'} . ∀x:{x:ℝ| x ∈ [a, b]} . (c' ≤ (g x))))
10. ∀c:ℝ. ((∀x:{x:ℝ| x ∈ [a, b]} . ((g x) < c)) ⇒ (∃c':{c':ℝ| c' < c} . ∀x:{x:ℝ| x ∈ [a, b]} . ((g x) ≤ c')))
11. bnd : ℝ
12. r0 ≤ bnd
13. ∀x:ℝ. ((x ∈ [a, b]) ⇒ (|g x| ≤ bnd))
⊢ ∃c,d:ℝ. ([c, d] ⊆ J  ∧ (∀x:{x:ℝ| x ∈ [a, b]} . (g[x] ∈ [c, d])))
BY
{ (D 7 THEN D 1 THEN DProdsAndUnions THEN All (Folds ``rccint rooint rcoint rocint``)⋅) }

1
1. x : ℝ
2. x2 : ℝ
3. n : ℕ⁺
4. a : ℝ
5. b : ℝ
6. a ≤ b
7. g : [a, b] ⟶ℝ
8. ∀x@0:{x:ℝ| x ∈ [a, b]} . (g[x@0] ∈ [x, x2])
9. ∀x,y:{x:ℝ| x ∈ [a, b]} .  g[x] = g[y] supposing x = y
10. real-fun(g;a;b)
11. ∀c:ℝ. ((∀x:{x:ℝ| x ∈ [a, b]} . (c < (g x))) ⇒ (∃c':{c':ℝ| c < c'} . ∀x:{x:ℝ| x ∈ [a, b]} . (c' ≤ (g x))))
12. ∀c:ℝ. ((∀x:{x:ℝ| x ∈ [a, b]} . ((g x) < c)) ⇒ (∃c':{c':ℝ| c' < c} . ∀x:{x:ℝ| x ∈ [a, b]} . ((g x) ≤ c')))
13. bnd : ℝ
14. r0 ≤ bnd
15. ∀x:ℝ. ((x ∈ [a, b]) ⇒ (|g x| ≤ bnd))
⊢ ∃c,d:ℝ. ([c, d] ⊆ [x, x2]  ∧ (∀x:{x:ℝ| x ∈ [a, b]} . (g[x] ∈ [c, d])))

2
1. y : ℝ
2. x2 : ℝ
3. n : ℕ⁺
4. a : ℝ
5. b : ℝ
6. a ≤ b
7. g : [a, b] ⟶ℝ
8. ∀x@0:{x:ℝ| x ∈ [a, b]} . (g[x@0] ∈ (y, x2])
9. ∀x,y:{x:ℝ| x ∈ [a, b]} .  g[x] = g[y] supposing x = y
10. real-fun(g;a;b)
11. ∀c:ℝ. ((∀x:{x:ℝ| x ∈ [a, b]} . (c < (g x))) ⇒ (∃c':{c':ℝ| c < c'} . ∀x:{x:ℝ| x ∈ [a, b]} . (c' ≤ (g x))))
12. ∀c:ℝ. ((∀x:{x:ℝ| x ∈ [a, b]} . ((g x) < c)) ⇒ (∃c':{c':ℝ| c' < c} . ∀x:{x:ℝ| x ∈ [a, b]} . ((g x) ≤ c')))
13. bnd : ℝ
14. r0 ≤ bnd
15. ∀x:ℝ. ((x ∈ [a, b]) ⇒ (|g x| ≤ bnd))
⊢ ∃c,d:ℝ. ([c, d] ⊆ (y, x2]  ∧ (∀x:{x:ℝ| x ∈ [a, b]} . (g[x] ∈ [c, d])))

3
1. x : ℝ
2. y : ℝ
3. n : ℕ⁺
4. a : ℝ
5. b : ℝ
6. a ≤ b
7. g : [a, b] ⟶ℝ
8. ∀x@0:{x:ℝ| x ∈ [a, b]} . (g[x@0] ∈ [x, y))
9. ∀x,y:{x:ℝ| x ∈ [a, b]} .  g[x] = g[y] supposing x = y
10. real-fun(g;a;b)
11. ∀c:ℝ. ((∀x:{x:ℝ| x ∈ [a, b]} . (c < (g x))) ⇒ (∃c':{c':ℝ| c < c'} . ∀x:{x:ℝ| x ∈ [a, b]} . (c' ≤ (g x))))
12. ∀c:ℝ. ((∀x:{x:ℝ| x ∈ [a, b]} . ((g x) < c)) ⇒ (∃c':{c':ℝ| c' < c} . ∀x:{x:ℝ| x ∈ [a, b]} . ((g x) ≤ c')))
13. bnd : ℝ
14. r0 ≤ bnd
15. ∀x:ℝ. ((x ∈ [a, b]) ⇒ (|g x| ≤ bnd))
⊢ ∃c,d:ℝ. ([c, d] ⊆ [x, y)  ∧ (∀x:{x:ℝ| x ∈ [a, b]} . (g[x] ∈ [c, d])))

4
1. y1 : ℝ
2. y : ℝ
3. n : ℕ⁺
4. a : ℝ
5. b : ℝ
6. a ≤ b
7. g : [a, b] ⟶ℝ
8. ∀x@0:{x:ℝ| x ∈ [a, b]} . (g[x@0] ∈ (y1, y))
9. ∀x,y:{x:ℝ| x ∈ [a, b]} .  g[x] = g[y] supposing x = y
10. real-fun(g;a;b)
11. ∀c:ℝ. ((∀x:{x:ℝ| x ∈ [a, b]} . (c < (g x))) ⇒ (∃c':{c':ℝ| c < c'} . ∀x:{x:ℝ| x ∈ [a, b]} . (c' ≤ (g x))))
12. ∀c:ℝ. ((∀x:{x:ℝ| x ∈ [a, b]} . ((g x) < c)) ⇒ (∃c':{c':ℝ| c' < c} . ∀x:{x:ℝ| x ∈ [a, b]} . ((g x) ≤ c')))
13. bnd : ℝ
14. r0 ≤ bnd
15. ∀x:ℝ. ((x ∈ [a, b]) ⇒ (|g x| ≤ bnd))
⊢ ∃c,d:ℝ. ([c, d] ⊆ (y1, y)  ∧ (∀x:{x:ℝ| x ∈ [a, b]} . (g[x] ∈ [c, d])))

5
1. y : Top
2. x1 : ℝ
3. n : ℕ⁺
4. a : ℝ
5. b : ℝ
6. a ≤ b
7. g : [a, b] ⟶ℝ
8. ∀x@0:{x:ℝ| x ∈ [a, b]} . (g[x@0] ∈ <inr y , inl inl x1>)
9. ∀x,y:{x:ℝ| x ∈ [a, b]} .  g[x] = g[y] supposing x = y
10. real-fun(g;a;b)
11. ∀c:ℝ. ((∀x:{x:ℝ| x ∈ [a, b]} . (c < (g x))) ⇒ (∃c':{c':ℝ| c < c'} . ∀x:{x:ℝ| x ∈ [a, b]} . (c' ≤ (g x))))
12. ∀c:ℝ. ((∀x:{x:ℝ| x ∈ [a, b]} . ((g x) < c)) ⇒ (∃c':{c':ℝ| c' < c} . ∀x:{x:ℝ| x ∈ [a, b]} . ((g x) ≤ c')))
13. bnd : ℝ
14. r0 ≤ bnd
15. ∀x:ℝ. ((x ∈ [a, b]) ⇒ (|g x| ≤ bnd))

⊢ ∃c,d:ℝ. ([c, d] ⊆ <inr y , inl inl x1>  ∧ (∀x:{x:ℝ| x ∈ [a, b]} . (g[x] ∈ [c, d])))

6
1. y : Top
2. y1 : ℝ
3. n : ℕ⁺
4. a : ℝ
5. b : ℝ
6. a ≤ b
7. g : [a, b] ⟶ℝ
8. ∀x@0:{x:ℝ| x ∈ [a, b]} . (g[x@0] ∈ <inr y , inl (inr y1 )>)
9. ∀x,y:{x:ℝ| x ∈ [a, b]} . g[x] = g[y] supposing x = y
10. real-fun(g;a;b)
11. ∀c:ℝ. ((∀x:{x:ℝ| x ∈ [a, b]} . (c < (g x))) ⇒ (∃c':{c':ℝ| c < c'} . ∀x:{x:ℝ| x ∈ [a, b]} . (c' ≤ (g x))))
12. ∀c:ℝ. ((∀x:{x:ℝ| x ∈ [a, b]} . ((g x) < c)) ⇒ (∃c':{c':ℝ| c' < c} . ∀x:{x:ℝ| x ∈ [a, b]} . ((g x) ≤ c')))
13. bnd : ℝ
14. r0 ≤ bnd
15. ∀x:ℝ. ((x ∈ [a, b]) ⇒ (|g x| ≤ bnd))

⊢ ∃c,d:ℝ. ([c, d] ⊆ <inr y , inl (inr y1 )>  ∧ (∀x:{x:ℝ| x ∈ [a, b]} . (g[x] ∈ [c, d])))

7
1. x1 : ℝ
2. y : Top
3. n : ℕ⁺
4. a : ℝ
5. b : ℝ
6. a ≤ b
7. g : [a, b] ⟶ℝ
8. ∀x@0:{x:ℝ| x ∈ [a, b]} . (g[x@0] ∈ <inl inl x1, inr y >)
9. ∀x,y:{x:ℝ| x ∈ [a, b]} . g[x] = g[y] supposing x = y
10. real-fun(g;a;b)
11. ∀c:ℝ. ((∀x:{x:ℝ| x ∈ [a, b]} . (c < (g x))) ⇒ (∃c':{c':ℝ| c < c'} . ∀x:{x:ℝ| x ∈ [a, b]} . (c' ≤ (g x))))
12. ∀c:ℝ. ((∀x:{x:ℝ| x ∈ [a, b]} . ((g x) < c)) ⇒ (∃c':{c':ℝ| c' < c} . ∀x:{x:ℝ| x ∈ [a, b]} . ((g x) ≤ c')))
13. bnd : ℝ
14. r0 ≤ bnd
15. ∀x:ℝ. ((x ∈ [a, b]) ⇒ (|g x| ≤ bnd))

⊢ ∃c,d:ℝ. ([c, d] ⊆ <inl inl x1, inr y >  ∧ (∀x:{x:ℝ| x ∈ [a, b]} . (g[x] ∈ [c, d])))

8
1. y1 : ℝ
2. y : Top
3. n : ℕ⁺
4. a : ℝ
5. b : ℝ
6. a ≤ b
7. g : [a, b] ⟶ℝ
8. ∀x@0:{x:ℝ| x ∈ [a, b]} . (g[x@0] ∈ <inl (inr y1 ), inr y >)
9. ∀x,y:{x:ℝ| x ∈ [a, b]} . g[x] = g[y] supposing x = y
10. real-fun(g;a;b)
11. ∀c:ℝ. ((∀x:{x:ℝ| x ∈ [a, b]} . (c < (g x))) ⇒ (∃c':{c':ℝ| c < c'} . ∀x:{x:ℝ| x ∈ [a, b]} . (c' ≤ (g x))))
12. ∀c:ℝ. ((∀x:{x:ℝ| x ∈ [a, b]} . ((g x) < c)) ⇒ (∃c':{c':ℝ| c' < c} . ∀x:{x:ℝ| x ∈ [a, b]} . ((g x) ≤ c')))
13. bnd : ℝ
14. r0 ≤ bnd
15. ∀x:ℝ. ((x ∈ [a, b]) ⇒ (|g x| ≤ bnd))

⊢ ∃c,d:ℝ. ([c, d] ⊆ <inl (inr y1 ), inr y >  ∧ (∀x:{x:ℝ| x ∈ [a, b]} . (g[x] ∈ [c, d])))

9
1. y1 : Top
2. y : Top
3. n : ℕ⁺
4. a : ℝ
5. b : ℝ
6. a ≤ b
7. g : [a, b] ⟶ℝ
8. ∀x:{x:ℝ| x ∈ [a, b]} . (g[x] ∈ <inr y1 , inr y >)
9. ∀x,y:{x:ℝ| x ∈ [a, b]} . g[x] = g[y] supposing x = y
10. real-fun(g;a;b)
11. ∀c:ℝ. ((∀x:{x:ℝ| x ∈ [a, b]} . (c < (g x))) ⇒ (∃c':{c':ℝ| c < c'} . ∀x:{x:ℝ| x ∈ [a, b]} . (c' ≤ (g x))))
12. ∀c:ℝ. ((∀x:{x:ℝ| x ∈ [a, b]} . ((g x) < c)) ⇒ (∃c':{c':ℝ| c' < c} . ∀x:{x:ℝ| x ∈ [a, b]} . ((g x) ≤ c')))
13. bnd : ℝ
14. r0 ≤ bnd
15. ∀x:ℝ. ((x ∈ [a, b]) ⇒ (|g x| ≤ bnd))

⊢ ∃c,d:ℝ. ([c, d] ⊆ <inr y1 , inr y >  ∧ (∀x:{x:ℝ| x ∈ [a, b]} . (g[x] ∈ [c, d])))

Latex:

Latex:
.....assertion..... 1. J : Interval 2. n : \mBbbN{}\msupplus{} 3. a : \mBbbR{} 4. b : \mBbbR{} 5. a \mleq{} b 6. g : [a, b] {}\mrightarrow{}\mBbbR{} 7. interval-fun([a, b];J;x.g[x]) 8. real-fun(g;a;b) 9. \mforall{}c:\mBbbR{} ((\mforall{}x:\{x:\mBbbR{}| x \mmember{} [a, b]\} . (c < (g x))) {}\mRightarrow{} (\mexists{}c':\{c':\mBbbR{}| c < c'\} . \mforall{}x:\{x:\mBbbR{}| x \mmember{} [a, b]\} . (c' \mleq{} (g x)))) 10. \mforall{}c:\mBbbR{} ((\mforall{}x:\{x:\mBbbR{}| x \mmember{} [a, b]\} . ((g x) < c)) {}\mRightarrow{} (\mexists{}c':\{c':\mBbbR{}| c' < c\} . \mforall{}x:\{x:\mBbbR{}| x \mmember{} [a, b]\} . ((g x) \mleq{} c'))) 11. bnd : \mBbbR{} 12. r0 \mleq{} bnd 13. \mforall{}x:\mBbbR{}. ((x \mmember{} [a, b]) {}\mRightarrow{} (|g x| \mleq{} bnd)) \mvdash{} \mexists{}c,d:\mBbbR{}. ([c, d] \msubseteq{} J \mwedge{} (\mforall{}x:\{x:\mBbbR{}| x \mmember{} [a, b]\} . (g[x] \mmember{} [c, d]))) By Latex: (D 7 THEN D 1 THEN DProdsAndUnions THEN All (Folds ``rccint rooint rcoint rocint``)\mcdot{}) Home Index