Step
*
1
1
1
1
1
1
1
of Lemma
cantor-to-interval-onto-common
1. a : ℝ
2. b : ℝ
3. [%] : a < b
4. x : ℝ
5. y : ℝ
6. x ∈ [a, b]
7. y ∈ [a, b]
8. n : ℕ
9. |x - y| ≤ (2^n * b - a)/6 * 3^n
10. ∀a,b:ℝ.
(((x ∈ [(2 * a + b)/3, b]) ∧ (y ∈ [(2 * a + b)/3, b]))
∨ ((x ∈ [a, (a + 2 * b)/3]) ∧ (y ∈ [a, (a + 2 * b)/3]))) supposing
(((x ∈ [a, b]) ∧ (y ∈ [a, b]) ∧ (|x - y| ≤ (b - a/r(6)))) and
(a < b))
11. m : ℕ
12. m + 1 ≠ 0
13. ∀m:ℕm. ∀f:ℕm ⟶ 𝔹.
∃g:ℕm + 1 ⟶ 𝔹 [((g = f ∈ (ℕm ⟶ 𝔹))
∧ (x ∈ [fst(cantor-interval(a;b;g;m + 1)), snd(cantor-interval(a;b;g;m + 1))])
∧ (y ∈ [fst(cantor-interval(a;b;g;m + 1)), snd(cantor-interval(a;b;g;m + 1))]))]
supposing (x ∈ [fst(cantor-interval(a;b;f;m)), snd(cantor-interval(a;b;f;m))])
∧ (y ∈ [fst(cantor-interval(a;b;f;m)), snd(cantor-interval(a;b;f;m))])
∧ (m ≤ n)
14. f : ℕm ⟶ 𝔹
15. (x ∈ [fst(cantor-interval(a;b;f;m)), snd(cantor-interval(a;b;f;m))])
∧ (y ∈ [fst(cantor-interval(a;b;f;m)), snd(cantor-interval(a;b;f;m))])
∧ (m ≤ n)
⊢ ∃g:ℕm + 1 ⟶ 𝔹 [((g = f ∈ (ℕm ⟶ 𝔹))
∧ (((fst(if m + 1 <z 1
then <a, b>
else let a',b' = cantor-interval(a;b;g;m)
in if g m then <(2 * a' + b')/3, b'> else <a', (a' + 2 * b')/3> fi
fi )) ≤ x)
∧ (x ≤ (snd(if m + 1 <z 1
then <a, b>
else let a',b' = cantor-interval(a;b;g;m)
in if g m then <(2 * a' + b')/3, b'> else <a', (a' + 2 * b')/3> fi
fi ))))
∧ ((fst(if m + 1 <z 1
then <a, b>
else let a',b' = cantor-interval(a;b;g;m)
in if g m then <(2 * a' + b')/3, b'> else <a', (a' + 2 * b')/3> fi
fi )) ≤ y)
∧ (y ≤ (snd(if m + 1 <z 1
then <a, b>
else let a',b' = cantor-interval(a;b;g;m)
in if g m then <(2 * a' + b')/3, b'> else <a', (a' + 2 * b')/3> fi
fi ))))]
BY
{ (InstHyp [⌜fst(cantor-interval(a;b;f;m))⌝;⌜snd(cantor-interval(a;b;f;m))⌝] 10⋅
THENA (Auto THEN Try ((BLemma `cantor-interval-rless` THEN Auto)))
) }
1
1. a : ℝ
2. b : ℝ
3. a < b
4. x : ℝ
5. y : ℝ
6. x ∈ [a, b]
7. y ∈ [a, b]
8. n : ℕ
9. |x - y| ≤ (2^n * b - a)/6 * 3^n
10. ∀a,b:ℝ.
(((x ∈ [(2 * a + b)/3, b]) ∧ (y ∈ [(2 * a + b)/3, b]))
∨ ((x ∈ [a, (a + 2 * b)/3]) ∧ (y ∈ [a, (a + 2 * b)/3]))) supposing
(((x ∈ [a, b]) ∧ (y ∈ [a, b]) ∧ (|x - y| ≤ (b - a/r(6)))) and
(a < b))
11. m : ℕ
12. m + 1 ≠ 0
13. ∀m:ℕm. ∀f:ℕm ⟶ 𝔹.
∃g:ℕm + 1 ⟶ 𝔹 [((g = f ∈ (ℕm ⟶ 𝔹))
∧ (x ∈ [fst(cantor-interval(a;b;g;m + 1)), snd(cantor-interval(a;b;g;m + 1))])
∧ (y ∈ [fst(cantor-interval(a;b;g;m + 1)), snd(cantor-interval(a;b;g;m + 1))]))]
supposing (x ∈ [fst(cantor-interval(a;b;f;m)), snd(cantor-interval(a;b;f;m))])
∧ (y ∈ [fst(cantor-interval(a;b;f;m)), snd(cantor-interval(a;b;f;m))])
∧ (m ≤ n)
14. f : ℕm ⟶ 𝔹
15. x ∈ [fst(cantor-interval(a;b;f;m)), snd(cantor-interval(a;b;f;m))]
16. y ∈ [fst(cantor-interval(a;b;f;m)), snd(cantor-interval(a;b;f;m))]
17. m ≤ n
18. x ∈ [fst(cantor-interval(a;b;f;m)), snd(cantor-interval(a;b;f;m))]
19. y ∈ [fst(cantor-interval(a;b;f;m)), snd(cantor-interval(a;b;f;m))]
⊢ |x - y| ≤ ((snd(cantor-interval(a;b;f;m))) - fst(cantor-interval(a;b;f;m))/r(6))
2
1. a : ℝ
2. b : ℝ
3. [%] : a < b
4. x : ℝ
5. y : ℝ
6. x ∈ [a, b]
7. y ∈ [a, b]
8. n : ℕ
9. |x - y| ≤ (2^n * b - a)/6 * 3^n
10. ∀a,b:ℝ.
(((x ∈ [(2 * a + b)/3, b]) ∧ (y ∈ [(2 * a + b)/3, b]))
∨ ((x ∈ [a, (a + 2 * b)/3]) ∧ (y ∈ [a, (a + 2 * b)/3]))) supposing
(((x ∈ [a, b]) ∧ (y ∈ [a, b]) ∧ (|x - y| ≤ (b - a/r(6)))) and
(a < b))
11. m : ℕ
12. m + 1 ≠ 0
13. ∀m:ℕm. ∀f:ℕm ⟶ 𝔹.
∃g:ℕm + 1 ⟶ 𝔹 [((g = f ∈ (ℕm ⟶ 𝔹))
∧ (x ∈ [fst(cantor-interval(a;b;g;m + 1)), snd(cantor-interval(a;b;g;m + 1))])
∧ (y ∈ [fst(cantor-interval(a;b;g;m + 1)), snd(cantor-interval(a;b;g;m + 1))]))]
supposing (x ∈ [fst(cantor-interval(a;b;f;m)), snd(cantor-interval(a;b;f;m))])
∧ (y ∈ [fst(cantor-interval(a;b;f;m)), snd(cantor-interval(a;b;f;m))])
∧ (m ≤ n)
14. f : ℕm ⟶ 𝔹
15. (x ∈ [fst(cantor-interval(a;b;f;m)), snd(cantor-interval(a;b;f;m))])
∧ (y ∈ [fst(cantor-interval(a;b;f;m)), snd(cantor-interval(a;b;f;m))])
∧ (m ≤ n)
16. ((x ∈ [(2 * fst(cantor-interval(a;b;f;m)) + (snd(cantor-interval(a;b;f;m))))/3, snd(cantor-interval(a;b;f;m))])
∧ (y ∈ [(2 * fst(cantor-interval(a;b;f;m)) + (snd(cantor-interval(a;b;f;m))))/3, snd(cantor-interval(a;b;f;m))]))
∨ ((x ∈ [fst(cantor-interval(a;b;f;m)), ((fst(cantor-interval(a;b;f;m))) + 2 * snd(cantor-interval(a;b;f;m)))/3])
∧ (y ∈ [fst(cantor-interval(a;b;f;m)), ((fst(cantor-interval(a;b;f;m))) + 2 * snd(cantor-interval(a;b;f;m)))/3]))
⊢ ∃g:ℕm + 1 ⟶ 𝔹 [((g = f ∈ (ℕm ⟶ 𝔹))
∧ (((fst(if m + 1 <z 1
then <a, b>
else let a',b' = cantor-interval(a;b;g;m)
in if g m then <(2 * a' + b')/3, b'> else <a', (a' + 2 * b')/3> fi
fi )) ≤ x)
∧ (x ≤ (snd(if m + 1 <z 1
then <a, b>
else let a',b' = cantor-interval(a;b;g;m)
in if g m then <(2 * a' + b')/3, b'> else <a', (a' + 2 * b')/3> fi
fi ))))
∧ ((fst(if m + 1 <z 1
then <a, b>
else let a',b' = cantor-interval(a;b;g;m)
in if g m then <(2 * a' + b')/3, b'> else <a', (a' + 2 * b')/3> fi
fi )) ≤ y)
∧ (y ≤ (snd(if m + 1 <z 1
then <a, b>
else let a',b' = cantor-interval(a;b;g;m)
in if g m then <(2 * a' + b')/3, b'> else <a', (a' + 2 * b')/3> fi
fi ))))]
Latex:
Latex:
1. a : \mBbbR{}
2. b : \mBbbR{}
3. [\%] : a < b
4. x : \mBbbR{}
5. y : \mBbbR{}
6. x \mmember{} [a, b]
7. y \mmember{} [a, b]
8. n : \mBbbN{}
9. |x - y| \mleq{} (2\^{}n * b - a)/6 * 3\^{}n
10. \mforall{}a,b:\mBbbR{}.
(((x \mmember{} [(2 * a + b)/3, b]) \mwedge{} (y \mmember{} [(2 * a + b)/3, b]))
\mvee{} ((x \mmember{} [a, (a + 2 * b)/3]) \mwedge{} (y \mmember{} [a, (a + 2 * b)/3]))) supposing
(((x \mmember{} [a, b]) \mwedge{} (y \mmember{} [a, b]) \mwedge{} (|x - y| \mleq{} (b - a/r(6)))) and
(a < b))
11. m : \mBbbN{}
12. m + 1 \mneq{} 0
13. \mforall{}m:\mBbbN{}m. \mforall{}f:\mBbbN{}m {}\mrightarrow{} \mBbbB{}.
\mexists{}g:\mBbbN{}m + 1 {}\mrightarrow{} \mBbbB{} [((g = f)
\mwedge{} (x \mmember{} [fst(cantor-interval(a;b;g;m + 1)), snd(cantor-interval(a;b;g;m + 1))])
\mwedge{} (y \mmember{} [fst(cantor-interval(a;b;g;m + 1)), snd(cantor-interval(a;b;g;m
+ 1))]))]
supposing (x \mmember{} [fst(cantor-interval(a;b;f;m)), snd(cantor-interval(a;b;f;m))])
\mwedge{} (y \mmember{} [fst(cantor-interval(a;b;f;m)), snd(cantor-interval(a;b;f;m))])
\mwedge{} (m \mleq{} n)
14. f : \mBbbN{}m {}\mrightarrow{} \mBbbB{}
15. (x \mmember{} [fst(cantor-interval(a;b;f;m)), snd(cantor-interval(a;b;f;m))])
\mwedge{} (y \mmember{} [fst(cantor-interval(a;b;f;m)), snd(cantor-interval(a;b;f;m))])
\mwedge{} (m \mleq{} n)
\mvdash{} \mexists{}g:\mBbbN{}m + 1 {}\mrightarrow{} \mBbbB{} [((g = f)
\mwedge{} (((fst(if m + 1 <z 1
then <a, b>
else let a',b' = cantor-interval(a;b;g;m)
in if g m then <(2 * a' + b')/3, b'> else <a', (a' + 2 * b')/3> fi
fi )) \mleq{} x)
\mwedge{} (x \mleq{} (snd(if m + 1 <z 1
then <a, b>
else let a',b' = cantor-interval(a;b;g;m)
in if g m then <(2 * a' + b')/3, b'> else <a', (a' + 2 * b')/3> fi
fi ))))
\mwedge{} ((fst(if m + 1 <z 1
then <a, b>
else let a',b' = cantor-interval(a;b;g;m)
in if g m then <(2 * a' + b')/3, b'> else <a', (a' + 2 * b')/3> fi
fi )) \mleq{} y)
\mwedge{} (y \mleq{} (snd(if m + 1 <z 1
then <a, b>
else let a',b' = cantor-interval(a;b;g;m)
in if g m then <(2 * a' + b')/3, b'> else <a', (a' + 2 * b')/3> fi
fi ))))]
By
Latex:
(InstHyp [\mkleeneopen{}fst(cantor-interval(a;b;f;m))\mkleeneclose{};\mkleeneopen{}snd(cantor-interval(a;b;f;m))\mkleeneclose{}] 10\mcdot{}
THENA (Auto THEN Try ((BLemma `cantor-interval-rless` THEN Auto)))
)
Home
Index