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)

[tree]
shi2 ti3
is subclass of
  chou1 xiang4 de5  
is subclass of
  guan1 xi4  
is subclass of
  dan1 zhi2 guan1 xi4  
is subclass of
  han2 shu4  
is subclass of
[tree]
shi2 ti3
is subclass of
  chou1 xiang4 de5  
is subclass of
  guan1 xi4  
is subclass of
  er4 yuan2 guan1 xi4  
is subclass of
is subclass of
  yi1 yuan2 han2 shu4  
is subclass of
  yi1 dui4 yi1 han2 shu4  

Subclass(es)

shun4 xu4 han2 shu4 

Coordinate term(s)

yi1 yuan2 heng2 ding4 han2 shu4 liang4 

Axioms (1)

(=>
      (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))))))