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