---

Step * 1 1 of Lemma discrete-fun-invariant


1. A : Type
2. B : Type
3. f : {() ⊢ _:(discr(A) ⟶ discr(B))}
4. ∀[I:fset(ℕ)]. ∀[a:()(I)].  ((f I a) = (λJ,h,u. (f {} ⋅ {} 1 u)) ∈ (discr(A) ⟶ discr(B))(a))
5. I : fset(ℕ)
6. a : ()(I)
7. (f I a) = (λJ,h,u. (f {} ⋅ {} 1 u)) ∈ (discr(A) ⟶ discr(B))(a)
8. (f {} ⋅) = (λJ,h,u. (f {} ⋅ {} 1 u)) ∈ (discr(A) ⟶ discr(B))(⋅)
⊢ (f I a) = (f {} ⋅) ∈ (discr(A) ⟶ discr(B))(a)
BY
{ Assert ⌜(discr(A) ⟶ discr(B))(⋅) ⊆r (discr(A) ⟶ discr(B))(a)⌝⋅ }

1
.....assertion..... 
1. A : Type
2. B : Type
3. f : {() ⊢ _:(discr(A) ⟶ discr(B))}
4. ∀[I:fset(ℕ)]. ∀[a:()(I)].  ((f I a) = (λJ,h,u. (f {} ⋅ {} 1 u)) ∈ (discr(A) ⟶ discr(B))(a))
5. I : fset(ℕ)
6. a : ()(I)
7. (f I a) = (λJ,h,u. (f {} ⋅ {} 1 u)) ∈ (discr(A) ⟶ discr(B))(a)
8. (f {} ⋅) = (λJ,h,u. (f {} ⋅ {} 1 u)) ∈ (discr(A) ⟶ discr(B))(⋅)
⊢ (discr(A) ⟶ discr(B))(⋅) ⊆r (discr(A) ⟶ discr(B))(a)

2
1. A : Type
2. B : Type
3. f : {() ⊢ _:(discr(A) ⟶ discr(B))}
4. ∀[I:fset(ℕ)]. ∀[a:()(I)].  ((f I a) = (λJ,h,u. (f {} ⋅ {} 1 u)) ∈ (discr(A) ⟶ discr(B))(a))
5. I : fset(ℕ)
6. a : ()(I)
7. (f I a) = (λJ,h,u. (f {} ⋅ {} 1 u)) ∈ (discr(A) ⟶ discr(B))(a)
8. (f {} ⋅) = (λJ,h,u. (f {} ⋅ {} 1 u)) ∈ (discr(A) ⟶ discr(B))(⋅)
9. (discr(A) ⟶ discr(B))(⋅) ⊆r (discr(A) ⟶ discr(B))(a)
⊢ (f I a) = (f {} ⋅) ∈ (discr(A) ⟶ discr(B))(a)

---

Latex:

---

Latex:

1.  A  :  Type
2.  B  :  Type
3.  f  :  \{()  \mvdash{}  \_:(discr(A)  {}\mrightarrow{}  discr(B))\}
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))
\mvdash{}  (f  I  a)  =  (f  \{\}  \mcdot{})


By

---

Latex:
Assert  \mkleeneopen{}(discr(A)  {}\mrightarrow{}  discr(B))(\mcdot{})  \msubseteq{}r  (discr(A)  {}\mrightarrow{}  discr(B))(a)\mkleeneclose{}\mcdot{}

---

Home Index