---

Step * of Lemma biject-inverse

No Annotations
∀[A,B:Type]. ∀[f:A ⟶ B].  (Bij(A;B;f) ⇒ (∃g:B ⟶ A. ((∀b:B. ((f (g b)) = b ∈ B)) ∧ (∀a:A. ((g (f a)) = a ∈ A)))))
BY
{ (Auto THEN RenameVar `bi' (-1) THEN D 0 With ⌜bij_inv(bi)⌝  THEN Auto) }

1
1. A : Type
2. B : Type
3. f : A ⟶ B
4. bi : Bij(A;B;f)
5. b : B
⊢ (f (bij_inv(bi) b)) = b ∈ B

---

Latex:

---

Latex:
No  Annotations
\mforall{}[A,B:Type].  \mforall{}[f:A  {}\mrightarrow{}  B].
    (Bij(A;B;f)  {}\mRightarrow{}  (\mexists{}g:B  {}\mrightarrow{}  A.  ((\mforall{}b:B.  ((f  (g  b))  =  b))  \mwedge{}  (\mforall{}a:A.  ((g  (f  a))  =  a)))))


By

---

Latex:
(Auto  THEN  RenameVar  `bi'  (-1)  THEN  D  0  With  \mkleeneopen{}bij\_inv(bi)\mkleeneclose{}    THEN  Auto)

---

Home Index