Nuprl Definition : inv_funs
InvFuns(A;B;f;g) == ((g o f) = Id{A} ∈ (A ⟶ A)) ∧ ((f o g) = Id{B} ∈ (B ⟶ B))
Definitions occuring in Statement :
compose: f o g,
tidentity: Id{T},
and: P ∧ Q,
function: x:A ⟶ B[x],
equal: s = t ∈ T
Definitions occuring in definition :
and: P ∧ Q,
equal: s = t ∈ T,
function: x:A ⟶ B[x],
compose: f o g,
tidentity: Id{T}
FDL editor aliases :
inv_funs
Latex:
InvFuns(A;B;f;g) == ((g o f) = Id\{A\}) \mwedge{} ((f o g) = Id\{B\})
Date html generated:
2016_05_13-PM-04_04_38
Last ObjectModification:
2015_09_22-PM-05_45_49
Theory : fun_1
Home
Index