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.

Ontologie

SUMO / BASE-ONTOLOGY

Class(es)

třída

inheritable relation

binární predikát
is instance of

relace částečné uspořádání
is instance of

třída

inheritable relation

relace rozšířená na veličiny
is instance of

less than or equal to

Související termín(y)

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

Typy argumentů

lessThanOrEqualTo(veličina, veličina)

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"

Axiomy (10)

less than or equal to je trichotomizing on reálné číslo.

(trichotomizingOn lessThanOrEqualTo RealNumber)

number1 je menší než nebo roven number2 tehdy a jen tehdy pokud number1 se rovná number2 nebo number1 je menší než number2.

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

greater than or equal to je inverzní k less than or equal to.

(inverse greaterThanOrEqualTo lessThanOrEqualTo)

Jestliže "length of list" se rovná number1, potom pro všechny number2 platí: existuje item tak, že "number2th element of list" se rovná item tehdy a jen tehdy pokud number2 je menší než nebo roven number1.

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

list3 se rovná "list concatenate fn(list1,list2)" tehdy a jen tehdy pokud pro všechny number1,number2 platí: jestliže number1 je menší než nebo roven "length of list1" a number2 je menší než nebo roven "length of list2" a number1 je instancí třídy kladné celé číslo a number2 je instancí třídy kladné celé číslo, potom "number1th element of list3" se rovná "number1th element of list1" a ""("length of list1"+number2)"th element of list3" se rovná "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))))))

jestliže list1 starts list2,
potom pro všechny number1,number2 platí: jestliže "length of list1" se rovná number1 a number2 je menší než nebo roven number1, potom "number2th element of list1" se rovná "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)))))

Jestliže "floor fn(number)" se rovná int, potom neexistuje celé číslo otherint tak, že otherint je menší než nebo roven number a otherint je větší než int.

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

jestliže "maximal weighted path fn(node1,node2)" se rovná path a "path weight fn(path)" se rovná number,
potom pro všechny path2 platí: jestliže path2 je instancí třídy "graph path fn(node1,node2)" a "path weight fn(path2)" se rovná number2, potom number2 je menší než nebo roven 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 je instancí třídy "interval fn(from,to)" tehdy a jen tehdy pokud quantity je větší než nebo roven from a quantity je menší než nebo roven to.

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

Jestliže day je instancí třídy "number of month", potom number je menší než nebo roven .

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