---

Step * of Lemma free-vs-dim-0

∀S:Type. ((¬S) ⇒ (∀K:CRng. free-vs(K;S) ≅ 0))
BY
{ (Auto
   THEN (InstLemma `free-vs-unique` [⌜S⌝;⌜K⌝;⌜0⌝]⋅ THENA Auto)
   THEN D -1
   THEN Thin (-1)
   THEN (D -1 THENM EAuto 1)
   THEN (Subst' Point(0) ~ Unit 0 THENA Computation)
   THEN D 0 With ⌜λx.⋅⌝ 
   THEN Auto
   THEN Reduce 0) }

1
1. S : Type
2. ¬S
3. K : CRng
4. vs : VectorSpace(K)
5. f : S ⟶ Point(vs)
⊢ ∃!h:0 ⟶ vs. ∀s:S. ((h ⋅) = (f s) ∈ Point(vs))

---

Latex:

---

Latex:
\mforall{}S:Type.  ((\mneg{}S)  {}\mRightarrow{}  (\mforall{}K:CRng.  free-vs(K;S)  \mcong{}  0))


By

---

Latex:
(Auto
  THEN  (InstLemma  `free-vs-unique`  [\mkleeneopen{}S\mkleeneclose{};\mkleeneopen{}K\mkleeneclose{};\mkleeneopen{}0\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  D  -1
  THEN  Thin  (-1)
  THEN  (D  -1  THENM  EAuto  1)
  THEN  (Subst'  Point(0)  \msim{}  Unit  0  THENA  Computation)
  THEN  D  0  With  \mkleeneopen{}\mlambda{}x.\mcdot{}\mkleeneclose{} 
  THEN  Auto
  THEN  Reduce  0)

---

Home Index