---

Step * of Lemma function_functionality_wrt_equipollent_left

∀[A,B,C:Type].  (A ~ B ⇒ A ⟶ C ~ B ⟶ C)
BY
{ (Unfold `equipollent` 0
   THEN Auto
   THEN D -1
   THEN ((D -1 THEN (FLemma `surject-inverse` [-1])) THENA Auto)
   THEN ExRepD) }

1
1. [A] : Type
2. [B] : Type
3. [C] : Type
4. f : A ⟶ B
5. Inj(A;B;f)
6. Surj(A;B;f)
7. g : B ⟶ A
8. ∀x:B. ((f (g x)) = x ∈ B)
⊢ ∃f:(A ⟶ C) ⟶ B ⟶ C. Bij(A ⟶ C;B ⟶ C;f)

---

Latex:

---

Latex:
\mforall{}[A,B,C:Type].    (A  \msim{}  B  {}\mRightarrow{}  A  {}\mrightarrow{}  C  \msim{}  B  {}\mrightarrow{}  C)


By

---

Latex:
(Unfold  `equipollent`  0
  THEN  Auto
  THEN  D  -1
  THEN  ((D  -1  THEN  (FLemma  `surject-inverse`  [-1]))  THENA  Auto)
  THEN  ExRepD)

---

Home Index