---

Step * of Lemma fun_with_inv_is_bij2

∀[A,B:Type].  ∀f:A ⟶ B. ((∃g:B ⟶ A. InvFuns(A;B;f;g)) ⇒ Bij(A;B;f))
BY
{ ((Auto THEN D (-1)) THEN (InstLemma `fun_with_inv_is_bij` [⌜A⌝;⌜B⌝;⌜f⌝;⌜g⌝]⋅ THEN Auto)) }

---

Latex:

---

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


By

---

Latex:
((Auto  THEN  D  (-1))  THEN  (InstLemma  `fun\_with\_inv\_is\_bij`  [\mkleeneopen{}A\mkleeneclose{};\mkleeneopen{}B\mkleeneclose{};\mkleeneopen{}f\mkleeneclose{};\mkleeneopen{}g\mkleeneclose{}]\mcdot{}  THEN  Auto))

---

Home Index