---

Step * of Lemma discrete-fun-bijection

∀[A,B:Type].  Bij({() ⊢ _:(discr(A) ⟶ discr(B))};{() ⊢ _:discr(A ⟶ B)};λf.discrete-fun(f))
BY
{ (Auto THEN RepeatFor 2 (D 0) THEN Reduce 0 THEN Auto) }

1
1. A : Type
2. B : Type
3. a1 : {() ⊢ _:(discr(A) ⟶ discr(B))}
4. a2 : {() ⊢ _:(discr(A) ⟶ discr(B))}
5. discrete-fun(a1) = discrete-fun(a2) ∈ {() ⊢ _:discr(A ⟶ B)}
⊢ a1 = a2 ∈ {() ⊢ _:(discr(A) ⟶ discr(B))}

2
1. [A] : Type
2. [B] : Type
3. b : {() ⊢ _:discr(A ⟶ B)}
⊢ ∃a:{() ⊢ _:(discr(A) ⟶ discr(B))}. (discrete-fun(a) = b ∈ {() ⊢ _:discr(A ⟶ B)})

---

Latex:

---

Latex:
\mforall{}[A,B:Type].    Bij(\{()  \mvdash{}  \_:(discr(A)  {}\mrightarrow{}  discr(B))\};\{()  \mvdash{}  \_:discr(A  {}\mrightarrow{}  B)\};\mlambda{}f.discrete-fun(f))


By

---

Latex:
(Auto  THEN  RepeatFor  2  (D  0)  THEN  Reduce  0  THEN  Auto)

---

Home Index