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