Step
*
1
of Lemma
convex-comb_wf
1. I : Interval
2. x : ℝ
3. x ∈ I
4. y : ℝ
5. y ∈ I
6. r : ℝ
7. r0 ≤ r
8. s : ℝ
9. r0 ≤ s
10. r0 < (r + s)
⊢ ((r * x) + (s * y)/r + s) ∈ I
BY
{ ((RepeatFor 2 (D 1) THEN D 2)
THEN Try (DVar `x1')
THEN Try (DVar `x2')
THEN All (RepUR ``i-member``)
THEN Auto
THEN nRMul ⌜r + s⌝ 0⋅
THEN Auto) }
1
1. x3 : ℝ
2. x4 : ℝ
3. x : ℝ
4. x3 ≤ x
5. x ≤ x4
6. y : ℝ
7. x3 ≤ y
8. y ≤ x4
9. r : ℝ
10. r0 ≤ r
11. s : ℝ
12. r0 ≤ s
13. r0 < (r + s)
⊢ ((r * x3) + (s * x3)) ≤ ((r * x) + (s * y))
2
1. x3 : ℝ
2. x4 : ℝ
3. x : ℝ
4. x3 ≤ x
5. x ≤ x4
6. y : ℝ
7. x3 ≤ y
8. y ≤ x4
9. r : ℝ
10. r0 ≤ r
11. s : ℝ
12. r0 ≤ s
13. r0 < (r + s)
14. x3 ≤ ((r * x) + (s * y)/r + s)
⊢ ((r * x) + (s * y)) ≤ ((r * x4) + (s * x4))
3
1. x3 : ℝ
2. y1 : ℝ
3. x : ℝ
4. x3 ≤ x
5. x < y1
6. y : ℝ
7. x3 ≤ y
8. y < y1
9. r : ℝ
10. r0 ≤ r
11. s : ℝ
12. r0 ≤ s
13. r0 < (r + s)
⊢ ((r * x3) + (s * x3)) ≤ ((r * x) + (s * y))
4
1. x3 : ℝ
2. y1 : ℝ
3. x : ℝ
4. x3 ≤ x
5. x < y1
6. y : ℝ
7. x3 ≤ y
8. y < y1
9. r : ℝ
10. r0 ≤ r
11. s : ℝ
12. r0 ≤ s
13. r0 < (r + s)
14. x3 ≤ ((r * x) + (s * y)/r + s)
⊢ ((r * x) + (s * y)) < ((r * y1) + (s * y1))
5
1. y1 : ℝ
2. x3 : ℝ
3. x : ℝ
4. y1 < x
5. x ≤ x3
6. y : ℝ
7. y1 < y
8. y ≤ x3
9. r : ℝ
10. r0 ≤ r
11. s : ℝ
12. r0 ≤ s
13. r0 < (r + s)
⊢ ((r * y1) + (s * y1)) < ((r * x) + (s * y))
6
1. y1 : ℝ
2. x3 : ℝ
3. x : ℝ
4. y1 < x
5. x ≤ x3
6. y : ℝ
7. y1 < y
8. y ≤ x3
9. r : ℝ
10. r0 ≤ r
11. s : ℝ
12. r0 ≤ s
13. r0 < (r + s)
14. y1 < ((r * x) + (s * y)/r + s)
⊢ ((r * x) + (s * y)) ≤ ((r * x3) + (s * x3))
7
1. y1 : ℝ
2. y2 : ℝ
3. x : ℝ
4. y1 < x
5. x < y2
6. y : ℝ
7. y1 < y
8. y < y2
9. r : ℝ
10. r0 ≤ r
11. s : ℝ
12. r0 ≤ s
13. r0 < (r + s)
⊢ ((r * y1) + (s * y1)) < ((r * x) + (s * y))
8
1. y1 : ℝ
2. y2 : ℝ
3. x : ℝ
4. y1 < x
5. x < y2
6. y : ℝ
7. y1 < y
8. y < y2
9. r : ℝ
10. r0 ≤ r
11. s : ℝ
12. r0 ≤ s
13. r0 < (r + s)
14. y1 < ((r * x) + (s * y)/r + s)
⊢ ((r * x) + (s * y)) < ((r * y2) + (s * y2))
9
1. x2 : ℕ+ ⟶ ℤ
2. regular-seq(x2)
3. y1 : Top
4. x : ℝ
5. x2 ≤ x
6. y : ℝ
7. x2 ≤ y
8. r : ℝ
9. r0 ≤ r
10. s : ℝ
11. r0 ≤ s
12. r0 < (r + s)
⊢ ((r * x2) + (s * x2)) ≤ ((r * x) + (s * y))
10
1. y2 : ℝ
2. y1 : Top
3. x : ℝ
4. y2 < x
5. y : ℝ
6. y2 < y
7. r : ℝ
8. r0 ≤ r
9. s : ℝ
10. r0 ≤ s
11. r0 < (r + s)
⊢ ((r * y2) + (s * y2)) < ((r * x) + (s * y))
11
1. y1 : Top
2. x2 : ℕ+ ⟶ ℤ
3. regular-seq(x2)
4. x : ℝ
5. x ≤ x2
6. y : ℝ
7. y ≤ x2
8. r : ℝ
9. r0 ≤ r
10. s : ℝ
11. r0 ≤ s
12. r0 < (r + s)
⊢ ((r * x) + (s * y)) ≤ ((r * x2) + (s * x2))
12
1. y1 : Top
2. y2 : ℝ
3. x : ℝ
4. x < y2
5. y : ℝ
6. y < y2
7. r : ℝ
8. r0 ≤ r
9. s : ℝ
10. r0 ≤ s
11. r0 < (r + s)
⊢ ((r * x) + (s * y)) < ((r * y2) + (s * y2))
Latex:
Latex:
1. I : Interval
2. x : \mBbbR{}
3. x \mmember{} I
4. y : \mBbbR{}
5. y \mmember{} I
6. r : \mBbbR{}
7. r0 \mleq{} r
8. s : \mBbbR{}
9. r0 \mleq{} s
10. r0 < (r + s)
\mvdash{} ((r * x) + (s * y)/r + s) \mmember{} I
By
Latex:
((RepeatFor 2 (D 1) THEN D 2)
THEN Try (DVar `x1')
THEN Try (DVar `x2')
THEN All (RepUR ``i-member``)
THEN Auto
THEN nRMul \mkleeneopen{}r + s\mkleeneclose{} 0\mcdot{}
THEN Auto)
Home
Index