---

Step * 1 1 1 1 1 1 1 of Lemma discrete-fun-invariant


1. A : Type
2. B : Type
3. f : {() ⊢ _:<λI,a. {w:J:fset(ℕ) ⟶ f:J ⟶ I ⟶ u:A ⟶ B| 
                       ∀J,K:fset(ℕ). ∀f:J ⟶ I. ∀g:K ⟶ J. ∀u:A.  ((w J f u) = (w K f ⋅ g u) ∈ B)} 
               , λI,J,f,a,w,K,g. (w K f ⋅ g)
               >}
4. ∀[I:fset(ℕ)]. ∀[a:()(I)].
     ((f I a)
     = (λJ,h,u. (f {} ⋅ {} 1 u))
     ∈ {w:J:fset(ℕ) ⟶ f:J ⟶ I ⟶ u:A ⟶ B| 
        ∀J,K:fset(ℕ). ∀f:J ⟶ I. ∀g:K ⟶ J. ∀u:A.  ((w J f u) = (w K f ⋅ g u) ∈ B)} )
5. I : fset(ℕ)
6. a : ()(I)
7. (f I a)
= (λJ,h,u. (f {} ⋅ {} 1 u))
∈ {w:J:fset(ℕ) ⟶ f:J ⟶ I ⟶ u:A ⟶ B| ∀J,K:fset(ℕ). ∀f:J ⟶ I. ∀g:K ⟶ J. ∀u:A.  ((w J f u) = (w K f ⋅ g u) ∈ B)} 
8. (f {} ⋅)
= (λJ,h,u. (f {} ⋅ {} 1 u))
∈ {w:J:fset(ℕ) ⟶ f:J ⟶ {} ⟶ u:A ⟶ B| ∀J,K:fset(ℕ). ∀f:J ⟶ {}. ∀g:K ⟶ J. ∀u:A.  ((w J f u) = (w K f ⋅ g u) ∈ B)} 
9. x : J:fset(ℕ) ⟶ f:J ⟶ {} ⟶ u:A ⟶ B
10. ∀J,K:fset(ℕ). ∀f:J ⟶ {}. ∀g:K ⟶ J. ∀u:A.  ((x J f u) = (x K f ⋅ g u) ∈ B)
⊢ x ∈ J:fset(ℕ) ⟶ f:J ⟶ I ⟶ u:A ⟶ B
BY
{ RepeatFor 3 ((FunExt THENA Auto)) }

1
1. A : Type
2. B : Type
3. f : {() ⊢ _:<λI,a. {w:J:fset(ℕ) ⟶ f:J ⟶ I ⟶ u:A ⟶ B| 
                       ∀J,K:fset(ℕ). ∀f:J ⟶ I. ∀g:K ⟶ J. ∀u:A.  ((w J f u) = (w K f ⋅ g u) ∈ B)} 
               , λI,J,f,a,w,K,g. (w K f ⋅ g)
               >}
4. ∀[I:fset(ℕ)]. ∀[a:()(I)].
     ((f I a)
     = (λJ,h,u. (f {} ⋅ {} 1 u))
     ∈ {w:J:fset(ℕ) ⟶ f:J ⟶ I ⟶ u:A ⟶ B| 
        ∀J,K:fset(ℕ). ∀f:J ⟶ I. ∀g:K ⟶ J. ∀u:A.  ((w J f u) = (w K f ⋅ g u) ∈ B)} )
5. I : fset(ℕ)
6. a : ()(I)
7. (f I a)
= (λJ,h,u. (f {} ⋅ {} 1 u))
∈ {w:J:fset(ℕ) ⟶ f:J ⟶ I ⟶ u:A ⟶ B| ∀J,K:fset(ℕ). ∀f:J ⟶ I. ∀g:K ⟶ J. ∀u:A.  ((w J f u) = (w K f ⋅ g u) ∈ B)} 
8. (f {} ⋅)
= (λJ,h,u. (f {} ⋅ {} 1 u))
∈ {w:J:fset(ℕ) ⟶ f:J ⟶ {} ⟶ u:A ⟶ B| ∀J,K:fset(ℕ). ∀f:J ⟶ {}. ∀g:K ⟶ J. ∀u:A.  ((w J f u) = (w K f ⋅ g u) ∈ B)} 
9. x : J:fset(ℕ) ⟶ f:J ⟶ {} ⟶ u:A ⟶ B
10. ∀J,K:fset(ℕ). ∀f:J ⟶ {}. ∀g:K ⟶ J. ∀u:A.  ((x J f u) = (x K f ⋅ g u) ∈ B)
11. J : fset(ℕ)
12. f1 : J ⟶ I
13. u : A
⊢ x J f1 u ∈ B

---

Latex:

---

Latex:

1.  A  :  Type
2.  B  :  Type
3.  f  :  \{()  \mvdash{}  \_:<\mlambda{}I,a.  \{w:J:fset(\mBbbN{})  {}\mrightarrow{}  f:J  {}\mrightarrow{}  I  {}\mrightarrow{}  u:A  {}\mrightarrow{}  B| 
                                              \mforall{}J,K:fset(\mBbbN{}).  \mforall{}f:J  {}\mrightarrow{}  I.  \mforall{}g:K  {}\mrightarrow{}  J.  \mforall{}u:A.    ((w  J  f  u)  =  (w  K  f  \mcdot{}  g  u))\} 
                              ,  \mlambda{}I,J,f,a,w,K,g.  (w  K  f  \mcdot{}  g)
                              >\}
4.  \mforall{}[I:fset(\mBbbN{})].  \mforall{}[a:()(I)].    ((f  I  a)  =  (\mlambda{}J,h,u.  (f  \{\}  \mcdot{}  \{\}  1  u)))
5.  I  :  fset(\mBbbN{})
6.  a  :  ()(I)
7.  (f  I  a)  =  (\mlambda{}J,h,u.  (f  \{\}  \mcdot{}  \{\}  1  u))
8.  (f  \{\}  \mcdot{})  =  (\mlambda{}J,h,u.  (f  \{\}  \mcdot{}  \{\}  1  u))
9.  x  :  J:fset(\mBbbN{})  {}\mrightarrow{}  f:J  {}\mrightarrow{}  \{\}  {}\mrightarrow{}  u:A  {}\mrightarrow{}  B
10.  \mforall{}J,K:fset(\mBbbN{}).  \mforall{}f:J  {}\mrightarrow{}  \{\}.  \mforall{}g:K  {}\mrightarrow{}  J.  \mforall{}u:A.    ((x  J  f  u)  =  (x  K  f  \mcdot{}  g  u))
\mvdash{}  x  \mmember{}  J:fset(\mBbbN{})  {}\mrightarrow{}  f:J  {}\mrightarrow{}  I  {}\mrightarrow{}  u:A  {}\mrightarrow{}  B


By

---

Latex:
RepeatFor  3  ((FunExt  THENA  Auto))

---

Home Index