Step * 1 1 of Lemma discrete-fun-bijection


1. Type
2. Type
3. {() ⊢ _:(discr(A) ⟶ discr(B))}
4. {() ⊢ _:(discr(A) ⟶ discr(B))}
5. discrete-fun(f) discrete-fun(g) ∈ {() ⊢ _:discr(A ⟶ B)}
6. fset(ℕ)
7. ()(I)
⊢ f(a) g(a) ∈ (discr(A) ⟶ discr(B))(a)
BY
(Assert f(a) ∈ (discr(A) ⟶ discr(B))(a) BY
         Auto) }

1
1. Type
2. Type
3. {() ⊢ _:(discr(A) ⟶ discr(B))}
4. {() ⊢ _:(discr(A) ⟶ discr(B))}
5. discrete-fun(f) discrete-fun(g) ∈ {() ⊢ _:discr(A ⟶ B)}
6. fset(ℕ)
7. ()(I)
8. f(a) ∈ (discr(A) ⟶ discr(B))(a)
⊢ f(a) g(a) ∈ (discr(A) ⟶ discr(B))(a)


Latex:


Latex:

1.  A  :  Type
2.  B  :  Type
3.  f  :  \{()  \mvdash{}  \_:(discr(A)  {}\mrightarrow{}  discr(B))\}
4.  g  :  \{()  \mvdash{}  \_:(discr(A)  {}\mrightarrow{}  discr(B))\}
5.  discrete-fun(f)  =  discrete-fun(g)
6.  I  :  fset(\mBbbN{})
7.  a  :  ()(I)
\mvdash{}  f(a)  =  g(a)


By


Latex:
(Assert  f(a)  \mmember{}  (discr(A)  {}\mrightarrow{}  discr(B))(a)  BY
              Auto)




Home Index