---

Step * 1 of Lemma discrete-map-is-constant2


1. T : Type
2. I : fset(ℕ)
3. phi : 𝔽(I)
4. s : A:fset(ℕ) ⟶ {f:A ⟶ I| (phi f) = 1}  ⟶ T
5. ∀A,B:fset(ℕ). ∀g:B ⟶ A.  ((λx.(s A x)) = (λx.(s B x ⋅ g)) ∈ ({f:A ⟶ I| (phi f) = 1}  ⟶ T))
6. f : {f:I ⟶ I| (phi f) = 1} 
7. ∀[J:fset(ℕ)]. ∀[g:J ⟶ I].  ((phi g) = 1 ⇒ (g = f ⋅ g ∈ J ⟶ I))
⊢ s = (λJ,g. (s I f)) ∈ (A:fset(ℕ) ⟶ {f:A ⟶ I| (phi f) = 1}  ⟶ T)
BY
{ ((RepeatFor 2 ((FunExt THENA Auto)) THEN Reduce 0)
   THEN (InstHyp [⌜I⌝;⌜A⌝;⌜x⌝] (-5)⋅ THENA Auto)
   THEN (ApFunToHypEquands `Z' ⌜Z f⌝ ⌜T⌝ (-1) ⋅ THENA Auto)
   THEN Reduce -1
   THEN Symmetry
   THEN NthHypEq (-1)
   THEN RepeatFor 2 (EqCDA)
   THEN DVar  `x'
   THEN EqTypeCD
   THEN Auto) }

---

Latex:

---

Latex:

1.  T  :  Type
2.  I  :  fset(\mBbbN{})
3.  phi  :  \mBbbF{}(I)
4.  s  :  A:fset(\mBbbN{})  {}\mrightarrow{}  \{f:A  {}\mrightarrow{}  I|  (phi  f)  =  1\}    {}\mrightarrow{}  T
5.  \mforall{}A,B:fset(\mBbbN{}).  \mforall{}g:B  {}\mrightarrow{}  A.    ((\mlambda{}x.(s  A  x))  =  (\mlambda{}x.(s  B  x  \mcdot{}  g)))
6.  f  :  \{f:I  {}\mrightarrow{}  I|  (phi  f)  =  1\} 
7.  \mforall{}[J:fset(\mBbbN{})].  \mforall{}[g:J  {}\mrightarrow{}  I].    ((phi  g)  =  1  {}\mRightarrow{}  (g  =  f  \mcdot{}  g))
\mvdash{}  s  =  (\mlambda{}J,g.  (s  I  f))


By

---

Latex:
((RepeatFor  2  ((FunExt  THENA  Auto))  THEN  Reduce  0)
  THEN  (InstHyp  [\mkleeneopen{}I\mkleeneclose{};\mkleeneopen{}A\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{}]  (-5)\mcdot{}  THENA  Auto)
  THEN  (ApFunToHypEquands  `Z'  \mkleeneopen{}Z  f\mkleeneclose{}  \mkleeneopen{}T\mkleeneclose{}  (-1)  \mcdot{}  THENA  Auto)
  THEN  Reduce  -1
  THEN  Symmetry
  THEN  NthHypEq  (-1)
  THEN  RepeatFor  2  (EqCDA)
  THEN  DVar    `x'
  THEN  EqTypeCD
  THEN  Auto)

---

Home Index