Step
*
1
1
1
4
1
of Lemma
face-of-face-pairity
1. k : ℕ
2. a : ℚCube(k)
3. b : ℚCube(k)
4. c : ℚCube(k)
5. 1 < dim(c)
6. immediate-rc-face(k;a;b)
7. immediate-rc-face(k;b;c)
8. i1 : ℕk
9. dim(b i1) = 1 ∈ ℤ
10. ∀j:ℕk. ((¬(j = i1 ∈ ℤ)) ⇒ ((a j) = (b j) ∈ ℚInterval))
11. ((a i1) = [fst((b i1))] ∈ ℚInterval) ∨ ((a i1) = [snd((b i1))] ∈ ℚInterval)
12. i : ℕk
13. dim(c i) = 1 ∈ ℤ
14. ∀j:ℕk. ((¬(j = i ∈ ℤ)) ⇒ ((b j) = (c j) ∈ ℚInterval))
15. ((b i) = [fst((c i))] ∈ ℚInterval) ∨ ((b i) = [snd((c i))] ∈ ℚInterval)
16. dim(a) = (dim(c) - 2) ∈ ℤ
17. ↑Inhabited(a)
18. dim(b) = (dim(c) - 1) ∈ ℤ
19. ↑Inhabited(b)
20. ↑Inhabited(c)
21. λj.if (j =z i1) then a i1 else c j fi ∈ ℚCube(k)
22. ↑Inhabited(λj.if (j =z i1) then a i1 else c j fi )
23. ¬(i1 = i ∈ ℤ)
24. dim(λj.if (j =z i1) then a i1 else c j fi ) = (dim(c) - 1) ∈ ℤ
25. immediate-rc-face(k;a;λj.if (j =z i1) then a i1 else c j fi )
26. immediate-rc-face(k;λj.if (j =z i1) then a i1 else c j fi ;c)
27. ¬((λj.if (j =z i1) then a i1 else c j fi ) = b ∈ ℚCube(k))
28. y : ℚCube(k)
29. immediate-rc-face(k;a;y)
30. immediate-rc-face(k;y;c)
31. ¬(y = b ∈ ℚCube(k))
32. ∃i:ℕk
((dim(y i) = 1 ∈ ℤ)
∧ (∀j:ℕk. ((¬(j = i ∈ ℤ)) ⇒ ((a j) = (y j) ∈ ℚInterval)))
∧ (((a i) = [fst((y i))] ∈ ℚInterval) ∨ ((a i) = [snd((y i))] ∈ ℚInterval)))
33. ∃i:ℕk
((dim(c i) = 1 ∈ ℤ)
∧ (∀j:ℕk. ((¬(j = i ∈ ℤ)) ⇒ ((y j) = (c j) ∈ ℚInterval)))
∧ (((y i) = [fst((c i))] ∈ ℚInterval) ∨ ((y i) = [snd((c i))] ∈ ℚInterval)))
⊢ y = (λj.if (j =z i1) then a i1 else c j fi ) ∈ ℚCube(k)
BY
{ (ExRepD
THEN (Assert ¬(i2 = i3 ∈ ℤ) BY
((D 0 THENA Auto)
THEN Eliminate ⌜i2⌝⋅
THEN (Assert dim(y i3) = 0 ∈ ℤ BY
(D -2 THEN (RWO "-2" 0 THENA Auto) THEN RepUR ``rat-interval-dimension`` 0 THEN AutoSplit))
THEN Auto))
) }
1
1. k : ℕ
2. a : ℚCube(k)
3. b : ℚCube(k)
4. c : ℚCube(k)
5. 1 < dim(c)
6. immediate-rc-face(k;a;b)
7. immediate-rc-face(k;b;c)
8. i1 : ℕk
9. dim(b i1) = 1 ∈ ℤ
10. ∀j:ℕk. ((¬(j = i1 ∈ ℤ)) ⇒ ((a j) = (b j) ∈ ℚInterval))
11. ((a i1) = [fst((b i1))] ∈ ℚInterval) ∨ ((a i1) = [snd((b i1))] ∈ ℚInterval)
12. i : ℕk
13. dim(c i) = 1 ∈ ℤ
14. ∀j:ℕk. ((¬(j = i ∈ ℤ)) ⇒ ((b j) = (c j) ∈ ℚInterval))
15. ((b i) = [fst((c i))] ∈ ℚInterval) ∨ ((b i) = [snd((c i))] ∈ ℚInterval)
16. dim(a) = (dim(c) - 2) ∈ ℤ
17. ↑Inhabited(a)
18. dim(b) = (dim(c) - 1) ∈ ℤ
19. ↑Inhabited(b)
20. ↑Inhabited(c)
21. λj.if (j =z i1) then a i1 else c j fi ∈ ℚCube(k)
22. ↑Inhabited(λj.if (j =z i1) then a i1 else c j fi )
23. ¬(i1 = i ∈ ℤ)
24. dim(λj.if (j =z i1) then a i1 else c j fi ) = (dim(c) - 1) ∈ ℤ
25. immediate-rc-face(k;a;λj.if (j =z i1) then a i1 else c j fi )
26. immediate-rc-face(k;λj.if (j =z i1) then a i1 else c j fi ;c)
27. ¬((λj.if (j =z i1) then a i1 else c j fi ) = b ∈ ℚCube(k))
28. y : ℚCube(k)
29. immediate-rc-face(k;a;y)
30. immediate-rc-face(k;y;c)
31. ¬(y = b ∈ ℚCube(k))
32. i3 : ℕk
33. dim(y i3) = 1 ∈ ℤ
34. ∀j:ℕk. ((¬(j = i3 ∈ ℤ)) ⇒ ((a j) = (y j) ∈ ℚInterval))
35. ((a i3) = [fst((y i3))] ∈ ℚInterval) ∨ ((a i3) = [snd((y i3))] ∈ ℚInterval)
36. i2 : ℕk
37. dim(c i2) = 1 ∈ ℤ
38. ∀j:ℕk. ((¬(j = i2 ∈ ℤ)) ⇒ ((y j) = (c j) ∈ ℚInterval))
39. ((y i2) = [fst((c i2))] ∈ ℚInterval) ∨ ((y i2) = [snd((c i2))] ∈ ℚInterval)
40. ¬(i2 = i3 ∈ ℤ)
⊢ y = (λj.if (j =z i1) then a i1 else c j fi ) ∈ ℚCube(k)
Latex:
Latex:
1. k : \mBbbN{}
2. a : \mBbbQ{}Cube(k)
3. b : \mBbbQ{}Cube(k)
4. c : \mBbbQ{}Cube(k)
5. 1 < dim(c)
6. immediate-rc-face(k;a;b)
7. immediate-rc-face(k;b;c)
8. i1 : \mBbbN{}k
9. dim(b i1) = 1
10. \mforall{}j:\mBbbN{}k. ((\mneg{}(j = i1)) {}\mRightarrow{} ((a j) = (b j)))
11. ((a i1) = [fst((b i1))]) \mvee{} ((a i1) = [snd((b i1))])
12. i : \mBbbN{}k
13. dim(c i) = 1
14. \mforall{}j:\mBbbN{}k. ((\mneg{}(j = i)) {}\mRightarrow{} ((b j) = (c j)))
15. ((b i) = [fst((c i))]) \mvee{} ((b i) = [snd((c i))])
16. dim(a) = (dim(c) - 2)
17. \muparrow{}Inhabited(a)
18. dim(b) = (dim(c) - 1)
19. \muparrow{}Inhabited(b)
20. \muparrow{}Inhabited(c)
21. \mlambda{}j.if (j =\msubz{} i1) then a i1 else c j fi \mmember{} \mBbbQ{}Cube(k)
22. \muparrow{}Inhabited(\mlambda{}j.if (j =\msubz{} i1) then a i1 else c j fi )
23. \mneg{}(i1 = i)
24. dim(\mlambda{}j.if (j =\msubz{} i1) then a i1 else c j fi ) = (dim(c) - 1)
25. immediate-rc-face(k;a;\mlambda{}j.if (j =\msubz{} i1) then a i1 else c j fi )
26. immediate-rc-face(k;\mlambda{}j.if (j =\msubz{} i1) then a i1 else c j fi ;c)
27. \mneg{}((\mlambda{}j.if (j =\msubz{} i1) then a i1 else c j fi ) = b)
28. y : \mBbbQ{}Cube(k)
29. immediate-rc-face(k;a;y)
30. immediate-rc-face(k;y;c)
31. \mneg{}(y = b)
32. \mexists{}i:\mBbbN{}k
((dim(y i) = 1)
\mwedge{} (\mforall{}j:\mBbbN{}k. ((\mneg{}(j = i)) {}\mRightarrow{} ((a j) = (y j))))
\mwedge{} (((a i) = [fst((y i))]) \mvee{} ((a i) = [snd((y i))])))
33. \mexists{}i:\mBbbN{}k
((dim(c i) = 1)
\mwedge{} (\mforall{}j:\mBbbN{}k. ((\mneg{}(j = i)) {}\mRightarrow{} ((y j) = (c j))))
\mwedge{} (((y i) = [fst((c i))]) \mvee{} ((y i) = [snd((c i))])))
\mvdash{} y = (\mlambda{}j.if (j =\msubz{} i1) then a i1 else c j fi )
By
Latex:
(ExRepD
THEN (Assert \mneg{}(i2 = i3) BY
((D 0 THENA Auto)
THEN Eliminate \mkleeneopen{}i2\mkleeneclose{}\mcdot{}
THEN (Assert dim(y i3) = 0 BY
(D -2
THEN (RWO "-2" 0 THENA Auto)
THEN RepUR ``rat-interval-dimension`` 0
THEN AutoSplit))
THEN Auto))
)
Home
Index