Step
*
1
1
1
1
2
1
of Lemma
closures-meet'
1. P : Set(ℝ)
2. Q : Set(ℝ)
3. a0 : ℝ
4. b0 : ℝ
5. a0 ∈ P
6. b0 ∈ Q
7. a0 < b0
8. c : ℝ
9. r0 ≤ c
10. c < r1
11. ∀a,b:ℝ.
(((a ∈ P) ∧ (b ∈ Q) ∧ (a < b))
⇒ (∃a',b':ℝ. ((a' ∈ P) ∧ (b' ∈ Q) ∧ (a ≤ a') ∧ (a' < b') ∧ (b' ≤ b) ∧ ((b' - a') ≤ ((b - a) * c)))))
12. a : ℝ
13. b : ℝ
14. a3 : a ∈ P
15. a5 : b ∈ Q
16. a6 : a < b
17. a' : ℝ
18. b' : ℝ
19. a' ∈ P
20. b' ∈ Q
21. a ≤ a'
22. a' < b'
23. b' ≤ b
24. (b' - a') ≤ ((b - a) * c)
25. q : (a' ∈ P) ∧ (b' ∈ Q) ∧ (a' < b')
⊢ ∃abp':a:ℝ × b:ℝ × ((a ∈ P) ∧ (b ∈ Q) ∧ (a < b)). let a,b,p = <a, b, a3, a5, a6> in let a',b',p' = abp' in (a ≤ a') ∧ (\000Ca' < b') ∧ (b' ≤ b) ∧ ((b' - a') ≤ ((b - a) * c))
BY
{ (At ⌜Type⌝ (InstConcl [⌜<a', b', q>⌝])⋅ THEN Reduce 0) }
1
.....wf.....
1. P : Set(ℝ)
2. Q : Set(ℝ)
3. a0 : ℝ
4. b0 : ℝ
5. a0 ∈ P
6. b0 ∈ Q
7. a0 < b0
8. c : ℝ
9. r0 ≤ c
10. c < r1
11. ∀a,b:ℝ.
(((a ∈ P) ∧ (b ∈ Q) ∧ (a < b))
⇒ (∃a',b':ℝ. ((a' ∈ P) ∧ (b' ∈ Q) ∧ (a ≤ a') ∧ (a' < b') ∧ (b' ≤ b) ∧ ((b' - a') ≤ ((b - a) * c)))))
12. a : ℝ
13. b : ℝ
14. a3 : a ∈ P
15. a5 : b ∈ Q
16. a6 : a < b
17. a' : ℝ
18. b' : ℝ
19. a' ∈ P
20. b' ∈ Q
21. a ≤ a'
22. a' < b'
23. b' ≤ b
24. (b' - a') ≤ ((b - a) * c)
25. q : (a' ∈ P) ∧ (b' ∈ Q) ∧ (a' < b')
⊢ <a', b', q> ∈ a:ℝ × b:ℝ × ((a ∈ P) ∧ (b ∈ Q) ∧ (a < b))
2
1. P : Set(ℝ)
2. Q : Set(ℝ)
3. a0 : ℝ
4. b0 : ℝ
5. a0 ∈ P
6. b0 ∈ Q
7. a0 < b0
8. c : ℝ
9. r0 ≤ c
10. c < r1
11. ∀a,b:ℝ.
(((a ∈ P) ∧ (b ∈ Q) ∧ (a < b))
⇒ (∃a',b':ℝ. ((a' ∈ P) ∧ (b' ∈ Q) ∧ (a ≤ a') ∧ (a' < b') ∧ (b' ≤ b) ∧ ((b' - a') ≤ ((b - a) * c)))))
12. a : ℝ
13. b : ℝ
14. a3 : a ∈ P
15. a5 : b ∈ Q
16. a6 : a < b
17. a' : ℝ
18. b' : ℝ
19. a' ∈ P
20. b' ∈ Q
21. a ≤ a'
22. a' < b'
23. b' ≤ b
24. (b' - a') ≤ ((b - a) * c)
25. q : (a' ∈ P) ∧ (b' ∈ Q) ∧ (a' < b')
⊢ (a ≤ a') ∧ (a' < b') ∧ (b' ≤ b) ∧ ((b' - a') ≤ ((b - a) * c))
3
1. P : Set(ℝ)
2. Q : Set(ℝ)
3. a0 : ℝ
4. b0 : ℝ
5. a0 ∈ P
6. b0 ∈ Q
7. a0 < b0
8. c : ℝ
9. r0 ≤ c
10. c < r1
11. ∀a,b:ℝ.
(((a ∈ P) ∧ (b ∈ Q) ∧ (a < b))
⇒ (∃a',b':ℝ. ((a' ∈ P) ∧ (b' ∈ Q) ∧ (a ≤ a') ∧ (a' < b') ∧ (b' ≤ b) ∧ ((b' - a') ≤ ((b - a) * c)))))
12. a : ℝ
13. b : ℝ
14. a3 : a ∈ P
15. a5 : b ∈ Q
16. a6 : a < b
17. a' : ℝ
18. b' : ℝ
19. a' ∈ P
20. b' ∈ Q
21. a ≤ a'
22. a' < b'
23. b' ≤ b
24. (b' - a') ≤ ((b - a) * c)
25. q : (a' ∈ P) ∧ (b' ∈ Q) ∧ (a' < b')
26. abp' : a:ℝ × b:ℝ × ((a ∈ P) ∧ (b ∈ Q) ∧ (a < b))
⊢ istype(let a',b',p' = abp' in
(a ≤ a') ∧ (a' < b') ∧ (b' ≤ b) ∧ ((b' - a') ≤ ((b - a) * c)))
Latex:
Latex:
1. P : Set(\mBbbR{})
2. Q : Set(\mBbbR{})
3. a0 : \mBbbR{}
4. b0 : \mBbbR{}
5. a0 \mmember{} P
6. b0 \mmember{} Q
7. a0 < b0
8. c : \mBbbR{}
9. r0 \mleq{} c
10. c < r1
11. \mforall{}a,b:\mBbbR{}.
(((a \mmember{} P) \mwedge{} (b \mmember{} Q) \mwedge{} (a < b))
{}\mRightarrow{} (\mexists{}a',b':\mBbbR{}
((a' \mmember{} P) \mwedge{} (b' \mmember{} Q) \mwedge{} (a \mleq{} a') \mwedge{} (a' < b') \mwedge{} (b' \mleq{} b) \mwedge{} ((b' - a') \mleq{} ((b - a) * c)))))
12. a : \mBbbR{}
13. b : \mBbbR{}
14. a3 : a \mmember{} P
15. a5 : b \mmember{} Q
16. a6 : a < b
17. a' : \mBbbR{}
18. b' : \mBbbR{}
19. a' \mmember{} P
20. b' \mmember{} Q
21. a \mleq{} a'
22. a' < b'
23. b' \mleq{} b
24. (b' - a') \mleq{} ((b - a) * c)
25. q : (a' \mmember{} P) \mwedge{} (b' \mmember{} Q) \mwedge{} (a' < b')
\mvdash{} \mexists{}abp':a:\mBbbR{} \mtimes{} b:\mBbbR{} \mtimes{} ((a \mmember{} P) \mwedge{} (b \mmember{} Q) \mwedge{} (a < b))
let a,b,p = <a, b, a3, a5, a6> in
let a',b',p' = abp' in
(a \mleq{} a') \mwedge{} (a' < b') \mwedge{} (b' \mleq{} b) \mwedge{} ((b' - a') \mleq{} ((b - a) * c))
By
Latex:
(At \mkleeneopen{}Type\mkleeneclose{} (InstConcl [\mkleeneopen{}<a', b', q>\mkleeneclose{}])\mcdot{} THEN Reduce 0)
Home
Index