less than or equal to (lessThanOrEqualTo)

(lessThanOrEqualTo number1 number2) is true just in case the Quantity number1 is less than or equal to the Quantity number2.

Ontology

SUMO / BASE-ONTOLOGY

Class(es)

class

inheritable relation

binary predicate
is instance of

partial ordering relation
is instance of

class

inheritable relation

relation extended to quantities
is instance of

less than or equal to

Coordinate term(s)

addition fn division fn exponentiation fn max fn min fn multiplication fn reciprocal fn remainder fn round fn subtraction fn arc weight authors before or equal causes causes subclass citizen closed on connected contains information cooccur copy date decreases likelihood developmental form disjoint distributes documentation duration earlier editor element employs equal equivalence relation on exploits expressed in language faces family relation finishes frequency graph part greater than greater than or equal to has purpose has skill holds during holds obligation holds right hole identity element in list in scope of interest increases likelihood independent probability inhabits inhibits initial list instance inverse irreflexive on larger less than located material measure meets temporally modal attribute overlaps temporally parent part partial ordering on partly located path length possesses precondition prevents property publishes range range subclass refers reflexive on related internal concept sibling smaller starts sub attribute sub collection sub graph sub list sub process sub proposition subclass subrelation subsumes content class subsumes content instance successor attribute successor attribute closure temporal part time total ordering on trichotomizing on uses valence version

Type restrictions

lessThanOrEqualTo(quantity, quantity)

Related WordNet synsets

lower bound: (mathematics) a number equal to or less than any other number in a given set
at most, at the most: not more than; "spend at most $20 on the lunch"

Axioms (10)

less than or equal to is trichotomizing on real number.

(trichotomizingOn lessThanOrEqualTo RealNumber)

number1 is less than or equal to number2 if and only if number1 is equal to number2 or number1 is less than number2.

(<=>
      (lessThanOrEqualTo ?NUMBER1 ?NUMBER2)
      (or
            (equal ?NUMBER1 ?NUMBER2)
            (lessThan ?NUMBER1 ?NUMBER2)))

greater than or equal to is an inverse of less than or equal to.

(inverse greaterThanOrEqualTo lessThanOrEqualTo)

If "length of list" is equal to number1, then for all number2 holds: there exists item so that "number2th element of list" is equal to item if and only if number2 is less than or equal to number1.

(=>
      (equal
            (ListLengthFn ?LIST)
            ?NUMBER1)
      (forall
            (?NUMBER2)
            (<=>
                  (exists
                        (?ITEM)
                        (equal
                              (ListOrderFn ?LIST ?NUMBER2)
                              ?ITEM))
                  (lessThanOrEqualTo ?NUMBER2 ?NUMBER1))))

list3 is equal to "the list composed of list1 and list2" if and only if for all number1,number2 holds: if number1 is less than or equal to "length of list1" and number2 is less than or equal to "length of list2" and number1 is an instance of positive integer and number2 is an instance of positive integer, then "number1th element of list3" is equal to "number1th element of list1" and ""("length of list1"+number2)"th element of list3" is equal to "number2th element of list2".

(<=>
      (equal
            ?LIST3
            (ListConcatenateFn ?LIST1 ?LIST2))
      (forall
            (?NUMBER1 ?NUMBER2)
            (=>
                  (and
                        (lessThanOrEqualTo
                              ?NUMBER1
                              (ListLengthFn ?LIST1))
                        (lessThanOrEqualTo
                              ?NUMBER2
                              (ListLengthFn ?LIST2))
                        (instance ?NUMBER1 PositiveInteger)
                        (instance ?NUMBER2 PositiveInteger))
                  (and
                        (equal
                              (ListOrderFn ?LIST3 ?NUMBER1)
                              (ListOrderFn ?LIST1 ?NUMBER1))
                        (equal
                              (ListOrderFn
                                    ?LIST3
                                    (AdditionFn
                                          (ListLengthFn ?LIST1)
                                          ?NUMBER2))
                              (ListOrderFn ?LIST2 ?NUMBER2))))))

if list1 starts list2,
then for all number1,number2 holds: if "length of list1" is equal to number1 and number2 is less than or equal to number1, then "number2th element of list1" is equal to "number2th element of list2"

(=>
      (initialList ?LIST1 ?LIST2)
      (forall
            (?NUMBER1 ?NUMBER2)
            (=>
                  (and
                        (equal
                              (ListLengthFn ?LIST1)
                              ?NUMBER1)
                        (lessThanOrEqualTo ?NUMBER2 ?NUMBER1))
                  (equal
                        (ListOrderFn ?LIST1 ?NUMBER2)
                        (ListOrderFn ?LIST2 ?NUMBER2)))))

If "the largest integer less than or equal to number" is equal to int, then there doesn't exist integer otherint so that otherint is less than or equal to number and otherint is greater than int.

(=>
      (equal
            (FloorFn ?NUMBER)
            ?INT)
      (not
            (exists
                  (?OTHERINT)
                  (and
                        (instance ?OTHERINT Integer)
                        (lessThanOrEqualTo ?OTHERINT ?NUMBER)
                        (greaterThan ?OTHERINT ?INT)))))

if "the highest cost path between node1 and node2" is equal to path and "the value of path" is equal to number,
then for all path2 holds: if path2 is an instance of "the set of paths between node1 and node2" and "the value of path2" is equal to number2, then number2 is less than or equal to number1

(=>
      (and
            (equal
                  (MaximalWeightedPathFn ?NODE1 ?NODE2)
                  ?PATH)
            (equal
                  (PathWeightFn ?PATH)
                  ?NUMBER))
      (forall
            (?PATH2)
            (=>
                  (and
                        (instance
                              ?PATH2
                              (GraphPathFn ?NODE1 ?NODE2))
                        (equal
                              (PathWeightFn ?PATH2)
                              ?NUMBER2))
                  (lessThanOrEqualTo ?NUMBER2 ?NUMBER1))))

quantity is an instance of "the interval from from to to" if and only if quantity is greater than or equal to from and quantity is less than or equal to to.

(<=>
      (instance
            ?QUANTITY
            (IntervalFn ?FROM ?TO))
      (and
            (greaterThanOrEqualTo ?QUANTITY ?FROM)
            (lessThanOrEqualTo ?QUANTITY ?TO)))

If day is an instance of "the day number", then number is less than or equal to .

(=>
      (instance
            ?DAY
            (DayFn ?NUMBER ?MONTH))
      (lessThanOrEqualTo ?NUMBER 31))