OpenMath Content Dictionary: set3

Canonical URL:

http://www.openmath.org/cd/set3.ocd

CD File:

set3.ocd

CD as XML Encoded OpenMath:

set3.omcd

Defines:

big_intersect, big_union, cartesian_power, k_subsets, map_with_condition, map_with_target, map_with_target_and_condition, powerset

Date:

1999-05-10

Version:

1 (Revision 1)

Review Date:

2003-04-01

Status:

experimental

Uses CD:

relation1, set1, nums1, setname1

This CD defines more set functions.

big_intersect

Description:

This symbol is a unary function whose argument should be a collection C of subsets of a given set. When applied to C, it represents the intersection over all members of C.

Signatures:

sts

big_union

Description:

This symbol is a unary function whose argument should be a collection C of subsets of a given set. When applied to C, it represents the union over all members of C.

Signatures:

sts

cartesian_power

Description:

This symbol is a binary function whose first argument should be a set A and whose second argument should be a natural number k. When applied to A and k, it represents the Cartesian product of k copies of A.

Signatures:

sts

powerset

Description:

This symbol represents unary function whose argument should be a set. When applied to a set X, it represents the collection of all subsets of X.

Commented Mathematical property (CMP):

The intersection over all subsets of a given set X is the empty set.

Formal Mathematical property (FMP):

xml prefix mathml

<OMOBJ xmlns="http://www.openmath.org/OpenMath" version="2.0">
  <OMA><OMS cd="relation1" name="eq"/>
       <OMA><OMS cd="set3" name="big_intersect"/>
            <OMA><OMS cd="set3" name="powerset"/>
                 <OMV name="X"/>
            </OMA>
       </OMA>
       <OMS cd="set1" name="emptyset"/>
  </OMA>
</OMOBJ>

eq (big_intersect (powerset ( X) ) , emptyset)

$${\bigcap }_{\mathcal{P}\left(X\right)}=\varnothing$$

Signatures:

sts

k_subsets

Description:

This symbol represents a binary function whose first argument should be a set and whose second argument should be a natural number. When applied to a set X and a number k, it represents the collection of all subsets of X of size k.

Signatures:

sts

map_with_target

Description:

This symbol represents a function with three arguments. The first argument is a function assignment f (in the form of a lambda binding), the second argument is a set X on which the first argument f is defined. The third argument specifies the range Y of the function. The symbol is used to denote the image {f(x) in Y | x in X} of application of the function f on the elements of X (so as to form a subset of Y).

Example:

One may form a set in the following way. This gives the set {1^2, 2^2, ... , 10^2 }

xml prefix mathml

<OMOBJ xmlns="http://www.openmath.org/OpenMath" version="2.0">
  <OMA><OMS cd="set3" name="map_with_target"/>
      <OMBIND><OMS cd="fns1" name="lambda"/>
          <OMBVAR><OMV name="x"/></OMBVAR>
          <OMA><OMS cd="arith1" name="power"/>
               <OMV name="x"/>      <OMI> 2 </OMI>
          </OMA>
     </OMBIND>
     <OMA><OMS cd="interval1" name="integer_interval"/>
          <OMI> 1 </OMI>         <OMI> 10 </OMI>
     </OMA>
     <OMS name="Z" cd="setname1"/>
 </OMA>
</OMOBJ>

map_with_target (lambda [ x] . (power ( x, 2 ) ) , integer_interval ( 1 , 10 ) , Z)

$$"\; >\left\{x^2\in \mathbb{Z}\right|x\in [1,10]\}$$

Example:

The definition of a product of subsets X and Y of a group G:

xml prefix mathml

<OMOBJ xmlns="http://www.openmath.org/OpenMath" version="2.0">
     <OMA><OMS cd="relation1" name="eq"/>
          <OMA><OMS cd="arith1" name="times"/>
               <OMV name="X"/> <OMV name="Y"/>
          </OMA>
          <OMA><OMS cd="set3" name="map_with_target"/>
               <OMBIND><OMS cd="fns1" name="lambda"/>
                        <OMBVAR>      <OMV name="x"/>      <OMV name="y"/>  </OMBVAR>
                        <OMA><OMS cd="arith1" name="times"/>
                             <OMV name="x"/> <OMV name="y"/>
                        </OMA>
              </OMBIND>
              <OMA><OMS cd="set1" name="cartesian_product"/>
                   <OMV name="X"/>   <OMV name="Y"/>
              </OMA>
              <OMV name="G"/> 
         </OMA>
    </OMA>
</OMOBJ>

eq (times ( X, Y) , map_with_target (lambda [ x y ] . (times ( x, y) ) , cartesian_product ( X, Y) , G) )

$$XY="\; >\left\{xy\in G\right|xy\in X\times Y\}$$

Signatures:

sts

map_with_condition

Description:

This symbol represents a function with three arguments. The first argument is a function assignment f (in the form of a lambda binding), the second argument is a set X. The third argument specifies a Boolean function P on X defining the subset Z of X (so Z = {x in X| P(x)}) on which the first argument f is defined, The symbol is used to denote the image {f(x) | x in X and P(x)} of application of the function f on the elements of Z.

Example:

One may form a set in the following way. This gives the set {2^2, 4^2, ... , 10^2 }

xml prefix mathml

<OMOBJ xmlns="http://www.openmath.org/OpenMath" version="2.0">
  <OMA><OMS cd="set3" name="map_with_condition"/>
      <OMBIND><OMS cd="fns1" name="lambda"/>
          <OMBVAR><OMV name="x"/></OMBVAR>
          <OMA><OMS cd="arith1" name="power"/>
               <OMV name="x"/>      <OMI> 2 </OMI>
          </OMA>
     </OMBIND>
     <OMA><OMS cd="interval1" name="integer_interval"/>
          <OMI> 1 </OMI>         <OMI> 10 </OMI>
     </OMA>
      <OMBIND><OMS cd="fns1" name="lambda"/>
          <OMBVAR><OMV name="x"/></OMBVAR>
          <OMA><OMS cd="integer2" name="divides"/>
               <OMI> 2 </OMI><OMV name="x"/>      
          </OMA>
     </OMBIND>
 </OMA>
</OMOBJ>

map_with_condition (lambda [ x] . (power ( x, 2 ) ) , integer_interval ( 1 , 10 ) , lambda [ x] . (divides ( 2 , x) ) )

$$\left\{x^2\right|x\in [1,10]\wedge \left(2\right|x)\}$$

Signatures:

sts

map_with_target_and_condition

Description:

This symbol represents a function with four arguments. The first argument is a function assignment f (in the form of a lambda binding), the second argument is a set X on which the first argument f is defined. The third argument specifies the range Y of the function. The fourth argument specifies a Boolean function P on X defining the subset Z of X (so Z = {x in X| P(x)}) on which the first argument f is defined, The symbol is used to denote the image {f(x) in Y | x in X and P(x)} of application of the function f on the elements of Z.

Example:

One may form a set in the following way. This gives the set {1^2, 2^2, ... , 10^2 }

xml prefix mathml

<OMOBJ xmlns="http://www.openmath.org/OpenMath" version="2.0">
  <OMA><OMS cd="set3" name="map_with_target_and_condition"/>
       <OMBIND><OMS cd="fns1" name="lambda"/>
            <OMBVAR><OMV name="x"/></OMBVAR>
            <OMA><OMS cd="arith1" name="power"/>
                 <OMV name="x"/>      <OMI> 2 </OMI>
            </OMA>
       </OMBIND>
       <OMA><OMS cd="interval1" name="integer_interval"/>
            <OMI> 1 </OMI>         <OMI> 10 </OMI>
       </OMA>
       <OMS cd="setname1" name="Z"/>
       <OMBIND><OMS cd="fns1" name="lambda"/>
            <OMBVAR><OMV name="x"/></OMBVAR>
            <OMA><OMS cd="integer2" name="divides"/>
                 <OMI> 2 </OMI><OMV name="x"/>      
            </OMA>
       </OMBIND>
  </OMA>
</OMOBJ>

map_with_target_and_condition (lambda [ x] . (power ( x, 2 ) ) , integer_interval ( 1 , 10 ) , Z, lambda [ x] . (divides ( 2 , x) ) )

$$\left\{x^2\in \mathbb{Z}\right|x\in [1,10]\wedge \left(2\right|x)\}$$

Signatures:

sts