---

Step * of Lemma inv_funs-iff

∀[A,B:Type]. ∀[f:A ⟶ B]. ∀[g:B ⟶ A].  (InvFuns(A;B;f;g) ⇐⇒ (∀a:A. ((g (f a)) = a ∈ A)) ∧ (∀b:B. ((f (g b)) = b ∈ B)))
BY
{ (RepUR ``inv_funs tidentity identity`` 0 THEN Auto THEN Try ((Ext THEN Reduce 0 THEN Auto))) }

1
1. A : Type
2. B : Type
3. f : A ⟶ B
4. g : B ⟶ A
5. (g o f) = (λx.x) ∈ (A ⟶ A)
6. (f o g) = (λx.x) ∈ (B ⟶ B)
7. a : A
⊢ (g (f a)) = a ∈ A

2
1. A : Type
2. B : Type
3. f : A ⟶ B
4. g : B ⟶ A
5. (g o f) = (λx.x) ∈ (A ⟶ A)
6. (f o g) = (λx.x) ∈ (B ⟶ B)
7. b : B
⊢ (f (g b)) = b ∈ B

---

Latex:

---

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


By

---

Latex:
(RepUR  ``inv\_funs  tidentity  identity``  0  THEN  Auto  THEN  Try  ((Ext  THEN  Reduce  0  THEN  Auto)))

---

Home Index