Select language: english | cesky | deutsch | italiano | simplified chinese | traditional chinese | hindi Concept: English word: Home

# yi1 dui4 yi1 han2 shu4 (OneToOneFunction)

The Class of UnaryFunctions which are one to one. A function F is one to one just in case for all X, Y in the domain of F, if X is not identical to Y, then F(X) is not identical to F(Y).

## Ontology

SUMO / BASE-ONTOLOGY

## Superclass(es)

 shi2 ti3

chou1 xiang4 de5

guan1 xi4

dan1 zhi2 guan1 xi4

han2 shu4
 shi2 ti3

chou1 xiang4 de5

guan1 xi4

er4 yuan2 guan1 xi4

yi1 yuan2 han2 shu4

yi1 dui4 yi1 han2 shu4

## Subclass(es)

shun4 xu4 han2 shu4

## Coordinate term(s)

yi1 yuan2 heng2 ding4 han2 shu4 liang4

## Axioms (1)

• if fun shi4 yi1 dui4 yi1 han2 shu4 de5 shi2 li4,
• then for all arg1,arg2 holds: if fun de5 lun4 yuan2 shi4 class de5 shi2 li4 and arg1 shi4 class de5 shi2 li4 and arg2 shi4 class de5 shi2 li4 and arg1 deng3 yu1 arg2, then "fun(arg1)" deng3 yu1 "fun(arg2)"
• .
```(=>
(instance ?FUN OneToOneFunction)
(forall
(?ARG1 ?ARG2)
(=>
(and
(domain ?FUN 1 ?CLASS)
(instance ?ARG1 ?CLASS)
(instance ?ARG2 ?CLASS)
(not
(equal ?ARG1 ?ARG2)))
(not
(equal
(AssignmentFn ?FUN ?ARG1)
(AssignmentFn ?FUN ?ARG2))))))```