SUMO   View all facts   Glossary   Help
Entity > Abstract > Class > Relation > BinaryRelation > UnaryFunction > DomainFn
Next UnaryFunction: EndFn    Up: UnaryFunction    Previous UnaryFunction: DenominatorFn   

DomainFn
subjectfact 
DomainFndocumentation The domain of a BinaryRelation ?REL is the Class of all things that bear ?REL to something2001-11-30 13:34:06.0
has axiom 
(<=> 
    (instance ?FUN OneToOneFunction) 
    (forall (?ARG1 ?ARG2) 
       (=> 
          (and 
             (instance ?ARG1 (DomainFn ?FUN)) 
             (instance ?ARG2 (DomainFn ?FUN)) 
             (not (equal ?ARG1 ?ARG2))) 
          (not (equal (AssignmentFn ?FUN ?ARG1) (AssignmentFn ?FUN ?ARG2))))))
2001-11-30 13:34:06.0
has axiom 
(<=> 
    (instance ?INST1 (DomainFn ?REL))
    (exists (?INST2)
       (holds ?REL ?INST1 ?INST2)))
2001-11-30 13:34:06.0
has axiom 
(=>
    (distributes ?FUNCTION1 ?FUNCTION2)
    (forall (?INST1 ?INST2 ?INST3)
       (=>
          (and
             (instance ?INST1 (DomainFn ?FUNCTION1))
             (instance ?INST2 (DomainFn ?FUNCTION1))
             (instance ?INST3 (DomainFn ?FUNCTION1))
             (instance ?INST1 (DomainFn ?FUNCTION2))
             (instance ?INST2 (DomainFn ?FUNCTION2))
             (instance ?INST3 (DomainFn ?FUNCTION2)))
          (equal (AssignmentFn ?FUNCTION1 ?INST1 
                         (AssignmentFn ?FUNCTION2 ?INST2 ?INST3))
                 (AssignmentFn ?FUNCTION2 
                         (AssignmentFn ?FUNCTION1 ?INST1 ?INST2) 
                         (AssignmentFn ?FUNCTION1 ?INST1 ?INST3))))))
2001-11-30 13:34:06.0
has axiom 
(=>
    (identityElement ?FUNCTION ?ID)
    (forall (?INST)
       (=>
          (instance ?INST (DomainFn ?FUNCTION))
          (equal (AssignmentFn ?FUNCTION ?ID ?INST) ?INST))))
2001-11-30 13:34:06.0
has axiom 
(=>
    (instance ?FUNCTION AssociativeFunction)
    (forall (?INST1 ?INST2 ?INST3)
       (=>
          (and
             (instance ?INST1 (DomainFn ?FUNCTION))
             (instance ?INST2 (DomainFn ?FUNCTION))
             (instance ?INST3 (DomainFn ?FUNCTION)))
          (equal (AssignmentFn ?FUNCTION ?INST1 (AssignmentFn ?FUNCTION ?INST1 ?INST2))
              (AssignmentFn ?FUNCTION (AssignmentFn ?FUNCTION ?INST1 ?INST2) ?INST3)))))
2001-11-30 13:34:06.0
has axiom 
(=>
    (instance ?FUNCTION CommutativeFunction)
    (forall (?INST1 ?INST2)
       (=>
          (and
             (instance ?INST1 (DomainFn ?FUNCTION))
             (instance ?INST2 (DomainFn ?FUNCTION)))
          (equal (AssignmentFn ?FUNCTION ?INST1 ?INST2) 
                 (AssignmentFn ?FUNCTION ?INST2 ?INST1)))))
2001-11-30 13:34:06.0
has domain1 BinaryRelation2001-11-30 13:34:06.0
has range Class2001-11-30 13:34:06.0
is an instance of UnaryFunction2001-11-30 13:34:06.0
BinaryRelationis first domain of DomainFn2001-11-30 13:33:44.0
is first domain of equivalenceRelationOn2001-11-30 13:33:44.0
is first domain of inverse2001-11-30 13:33:44.0
is first domain of irreflexiveOn2001-11-30 13:33:44.0
is first domain of partialOrderingOn2001-11-30 13:33:44.0
is first domain of RangeFn2001-11-30 13:33:44.0
is first domain of reflexiveOn2001-11-30 13:33:44.0
is first domain of totalOrderingOn2001-11-30 13:33:44.0
is first domain of trichotomizingOn2001-11-30 13:33:44.0
is second domain of inverse2001-11-30 13:33:44.0
Functionis first domain of AssignmentFn2001-11-30 13:34:18.0
is first domain of closedOn2001-11-30 13:34:18.0
is first domain of range2001-11-30 13:34:18.0
is first domain of rangeSubclass2001-11-30 13:34:18.0
Classis third domain of domain2001-11-30 13:33:51.0
is third domain of domainSubclass2001-11-30 13:33:51.0
Abstractis disjoint from Physical2001-11-30 13:33:32.0

Next UnaryFunction: EndFn    Up: UnaryFunction    Previous UnaryFunction: DenominatorFn