WhoCites
Definitions
GenAutomata
Sections
NuprlLIB
Doc
Who Cites rel
inverse?
rel_inverse
Def R^-1(x,y) == y R x
Thm*
T1,T2:Type, R:(T1
T2
Prop). R^-1
T2
T1
Prop
Syntax:
R^-1
has structure:
rel_inverse(R)
About:
WhoCites
Definitions
GenAutomata
Sections
NuprlLIB
Doc