---

Step * of Lemma biject-inverse2

∀[A,B:Type].  ∀f:A ⟶ B. (Bij(A;B;f) ⇒ (∃g:B ⟶ A. InvFuns(A;B;f;g)))
BY
{ (Auto
   THEN FLemma `biject-inverse` [4]
   THEN Auto
   THEN D (-1)
   THEN InstConcl [⌜g⌝]⋅
   THEN Auto
   THEN D 0
   THEN RepUR ``tidentity identity`` 0
   THEN BetterExt
   THEN Auto
   THEN Reduce 0
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[A,B:Type].    \mforall{}f:A  {}\mrightarrow{}  B.  (Bij(A;B;f)  {}\mRightarrow{}  (\mexists{}g:B  {}\mrightarrow{}  A.  InvFuns(A;B;f;g)))


By

---

Latex:
(Auto
  THEN  FLemma  `biject-inverse`  [4]
  THEN  Auto
  THEN  D  (-1)
  THEN  InstConcl  [\mkleeneopen{}g\mkleeneclose{}]\mcdot{}
  THEN  Auto
  THEN  D  0
  THEN  RepUR  ``tidentity  identity``  0
  THEN  BetterExt
  THEN  Auto
  THEN  Reduce  0
  THEN  Auto)

---

Home Index