SUMO   View all facts   Glossary   Help
Entity > Abstract > Class > Relation > BinaryRelation > AntisymmetricRelation > AsymmetricRelation > closedOn
Next AsymmetricRelationcontains    UpAsymmetricRelation, BinaryPredicate    Previous AsymmetricRelationcitizen   

closedOn
subjectfact 
closedOndocumentation A BinaryFunction is closed on a Class if it is defined for all instances of the Class and its value is always an instance of the Class2001-11-30 13:33:51.0
has axiom
(=>
(and
(closedOn ?FUNCTION ?CLASS)
(instance ?FUNCTION UnaryFunction))
(forall (?INST)
(=>
(instance ?INST ?CLASS)
(instance (AssignmentFn ?FUNCTION ?INST) ?CLASS))))
2001-11-30 13:33:51.0
has axiom
(=>
(and
(closedOn ?FUNCTION ?CLASS)
(instance ?FUNCTION BinaryFunction))
(forall (?INST1 ?INST2)
(=>
(and
(instance ?INST1 ?CLASS)
(instance ?INST2 ?CLASS))
(instance (AssignmentFn ?FUNCTION ?INST1 ?INST2) ?CLASS))))
2001-11-30 13:33:51.0
has domain1 Function2001-11-30 13:33:51.0
has domain2 Class2001-11-30 13:33:51.0
is an instance of AsymmetricRelation2001-11-30 13:33:51.0
is an instance of BinaryPredicate2001-11-30 13:33:51.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
Predicateis first domain of singleValued2001-11-30 13:35:02.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 AsymmetricRelationcontains    UpAsymmetricRelation, BinaryPredicate    Previous AsymmetricRelationcitizen