---

Step * of Lemma 0-dim-complex-polyhedron-decidable

∀k:ℕ. ∀K:0-dim-complex. ∀x,y:|K|.  Dec(x ≡ y)
BY
{ (InstLemma `0-dim-complex-polyhedron` []
   THEN RepeatFor 2 (ParallelLast')
   THEN Intros
   THEN (InstHyp [⌜x⌝] 3⋅ THENA Auto)
   THEN (InstHyp [⌜y⌝] 3⋅ THENA Auto)
   THEN (RWO "meq-rn-prod-metric" 0 THENA Auto)
   THEN ExRepD
   THEN (InstLemma `req-vec_functionality` [⌜k⌝;⌜x⌝;⌜λj.rat2real(fst((K[i1] j)))⌝;⌜y⌝;⌜λj.rat2real(fst((K[i] j)))⌝]⋅
         THENA Auto
         )
   THEN RWO "-1" 0
   THEN Auto) }

1
.....decidable?..... 
1. k : ℕ
2. K : 0-dim-complex
3. ∀x:|K|. ∃i:ℕ||K||. req-vec(k;x;λj.rat2real(fst((K[i] j))))
4. x : |K|
5. y : |K|
6. i1 : ℕ||K||
7. req-vec(k;x;λj.rat2real(fst((K[i1] j))))
8. i : ℕ||K||
9. req-vec(k;y;λj.rat2real(fst((K[i] j))))
10. req-vec(k;λj.rat2real(fst((K[i1] j)));λj.rat2real(fst((K[i] j)))) supposing req-vec(k;x;y)
11. req-vec(k;x;y) supposing req-vec(k;λj.rat2real(fst((K[i1] j)));λj.rat2real(fst((K[i] j))))
⊢ Dec(req-vec(k;λj.rat2real(fst((K[i1] j)));λj.rat2real(fst((K[i] j)))))

---

Latex:

---

Latex:
\mforall{}k:\mBbbN{}.  \mforall{}K:0-dim-complex.  \mforall{}x,y:|K|.    Dec(x  \mequiv{}  y)


By

---

Latex:
(InstLemma  `0-dim-complex-polyhedron`  []
  THEN  RepeatFor  2  (ParallelLast')
  THEN  Intros
  THEN  (InstHyp  [\mkleeneopen{}x\mkleeneclose{}]  3\mcdot{}  THENA  Auto)
  THEN  (InstHyp  [\mkleeneopen{}y\mkleeneclose{}]  3\mcdot{}  THENA  Auto)
  THEN  (RWO  "meq-rn-prod-metric"  0  THENA  Auto)
  THEN  ExRepD
  THEN  (InstLemma  `req-vec\_functionality`  [\mkleeneopen{}k\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{};\mkleeneopen{}\mlambda{}j.rat2real(fst((K[i1]  j)))\mkleeneclose{};\mkleeneopen{}y\mkleeneclose{};
              \mkleeneopen{}\mlambda{}j.rat2real(fst((K[i]  j)))\mkleeneclose{}]\mcdot{}
              THENA  Auto
              )
  THEN  RWO  "-1"  0
  THEN  Auto)

---

Home Index