properties of LAMBHULL

Johan G. F. Belinfante
2003 October 21

<<  goedel52.t06; << tools.m

summary

This notebook contains derivations of some properties of the function LAMBHULL.   The meaning of this function is clear from these rules:

member[x, LAMBHULL]

image[LAMBHULL, singleton[x]]

The primary application of the function LAMBHULL is to provide variable-free formulations of theorems about HULL[x], valid for the case that  x  is a set.  The hope is that such results may eventually find applications in topology.

a new membership rule

The old rule is best removed (temporarily) for this derivation.  It can be restored later.

member[x_, LAMBHULL] =.

Lemma 1.

SubstTest[member, pair[x, y], composite[Id, z], z -> LAMBHULL] // 
      Reverse

and[member[x_, V], member[y_, V], member[pair[x_, y_], LAMBHULL]] := 
      member[pair[x, y], LAMBHULL]

Lemma 2.

SubstTest[implies, and[equal[y, z], member[y, V]], member[z, V], 
      z -> HULL[x]]

or[member[x_, V], not[equal[y_, HULL[x]]], not[member[y_, V]]] := 
      True

Lemma 3.

SubstTest[implies, and[equal[y, z], member[z, V]], member[y, V], 
      z -> HULL[x]]

or[member[y_, V], not[equal[y_, HULL[x_]]], not[member[x_, V]]] := 
      True

Corollary:

equiv[and[equal[y, HULL[x]], member[y, V]], 
      and[equal[y, HULL[x]], member[x, V]]]

and[equal[y_, HULL[x_]], member[y_, V]] := 
      and[equal[y, HULL[x]], member[x, V]]

This is the new membership rule:

SubstTest[member, y, image[z, singleton[x]], z -> LAMBHULL] // 
      Reverse

member[pair[x_, y_], LAMBHULL] := 
      and[equal[y, HULL[x]], member[x, V]]

a formula for LAMBHULL

In this section a variable-free version of this rule is derived:

HULL[image[inverse[S], x]]

Only one step is needed:

composite[LAMBHULL, IMAGE[inverse[S]]] // VSNormality

composite[LAMBHULL, IMAGE[inverse[S]]] := 
      composite[IMAGE[DUP], IMAGE[inverse[S]]]

HULL[singleton[x]]

In this section a variable-free version of the following formula is derived:

HULL[singleton[x]]

The function that takes  x  to  HULL[singleton[x]] is:

lambda[x, cart[P[x], singleton[x]]]

symdif[composite[LAMBHULL, SINGLETON], 
        VERTSECT[composite[id[S], inverse[SECOND]]]] // 
      VSNormality

union[
        intersection[complement[VERTSECT[composite[id[S], inverse[SECOND]]]], 
          composite[LAMBHULL, SINGLETON]], 
        intersection[composite[complement[LAMBHULL], SINGLETON], 
          VERTSECT[composite[id[S], inverse[SECOND]]]]] := 0

SubstTest[equal, 0, 
      symdif[u, v], {u -> composite[LAMBHULL, SINGLETON], 
        v -> VERTSECT[composite[id[S], inverse[SECOND]]]}]

composite[LAMBHULL, SINGLETON] := 
      VERTSECT[composite[id[S], inverse[SECOND]]]

There is another formula for this function:

\(symdif[
        composite[CART, 
          intersection[composite[inverse[FIRST], POWER], 
            composite[inverse[SECOND], SINGLETON]]], 
	
        VERTSECT[composite[id[S], inverse[SECOND]]]] // 
      VSNormality\)

union[
        intersection[complement[VERTSECT[composite[id[S], inverse[SECOND]]]], 
          composite[CART, 
            intersection[composite[inverse[FIRST], POWER], 
              composite[inverse[SECOND], SINGLETON]]]], 
        intersection[
          composite[complement[CART], 
            intersection[composite[inverse[FIRST], POWER], 
              composite[inverse[SECOND], SINGLETON]]], 
          VERTSECT[composite[id[S], inverse[SECOND]]]]] := 0

SubstTest[equal, 0, 
      symdif[u, v], {u -> VERTSECT[composite[id[S], inverse[SECOND]]], 
        v -> composite[CART, 
            intersection[composite[inverse[FIRST], POWER], 
              composite[inverse[SECOND], SINGLETON]]]}]

composite[CART, 
        intersection[composite[inverse[FIRST], POWER], 
          composite[inverse[SECOND], SINGLETON]]] := 
      VERTSECT[composite[id[S], inverse[SECOND]]]

range[LAMBHULL]

Map[subclass[#, FUNS] &, ImageComp[FUNPART, LAMBHULL, V]]

subclass[range[LAMBHULL], FUNS] := True

The formula derived in the preceding section implies:

ImageComp[composite[inverse[E], LAMBHULL], SINGLETON, V] // 
      Reverse

U[image[LAMBHULL, range[SINGLETON]]] := S

\(SubstTest[implies, subclass[u, v], 
      subclass[U[u], U[v]], 
	{u -> image[LAMBHULL, range[SINGLETON]], 
        v -> range[LAMBHULL]}]\)

subclass[S, U[range[LAMBHULL]]] := True

To derive the reverse inclusion, one needs to use this fact:

subclass[HULL[x], S]

dif[LAMBHULL, composite[id[P[S]], LAMBHULL]] // VSNormality

union[
        composite[LAMBHULL, id[complement[image[inverse[LAMBHULL], P[S]]]]], 
        composite[id[complement[P[S]]], LAMBHULL]] := 0

SubstTest[equal, 0, 
        symdif[u, v], {u -> composite[id[P[S]], LAMBHULL], v -> LAMBHULL}] // 
      Reverse

subclass[U[range[LAMBHULL]], S] := True

SubstTest[and, subclass[u, v], 
      subclass[v, u], {u -> U[range[LAMBHULL]], v -> S}]

U[range[LAMBHULL]] := S

Corollary:

equal[intersection[range[LAMBHULL], P[S]], range[LAMBHULL]]

intersection[P[S], range[LAMBHULL]] := range[LAMBHULL]

Assoc[id[P[S]], id[range[LAMBHULL]], LAMBHULL]

composite[id[P[S]], LAMBHULL] := LAMBHULL

monotonicity

Map[equal[0, #] &, 
        SubstTest[reify, x, dif[composite[F[x], S, inverse[F[x]]], S], 
          F -> HULL]] // Reverse

subclass[range[LAMBHULL], 
        cliques[complement[cross[S, complement[S]]]]] := True

the hereditary domain property

ImageComp[IMAGE[FIRST], LAMBHULL, V] // Reverse

image[IMAGE[FIRST], range[LAMBHULL]] := 
      fix[IMAGE[inverse[S]]]

using reify to derive a property of LAMBHULL

The goal is to obtain a variable-free version of this property of the constructor  HULL:

SubstTest[implies, equal[u, v], 
      equal[domain[u], domain[v]], {u -> HULL[x], v -> HULL[y]}]

In order to apply reify, one needs first to replace this statement with an equation for an object.  This is done as follows:

union[image[V, intersection[complement[HULL[x]], HULL[y]]], 
        image[V, intersection[complement[HULL[y]], HULL[x]]], 
        intersection[
          complement[
            image[V, intersection[x, complement[image[inverse[S], y]]]]], 
          complement[
            image[V, intersection[y, complement[image[inverse[S], x]]]]]]] // 
      Normality

The variables are now removed one by one using reify.

Map[domain[reify[x, #]] &, %]

Map[equal[0, composite[Id, complement[reify[y, #]]]] &, %]

subclass[composite[IMAGE[inverse[S]], inverse[LAMBHULL], LAMBHULL], 
        IMAGE[inverse[S]]] := True

The final result can be cleaned up a little:

\(SubstTest[implies, subclass[u, v], 
      subclass[composite[u, w], 
        composite[v, w]], 
	{u -> 
          composite[IMAGE[inverse[S]], inverse[LAMBHULL], LAMBHULL], 
        v -> IMAGE[inverse[S]], w -> inverse[IMAGE[inverse[S]]]}]\)

subclass[
        composite[IMAGE[inverse[S]], inverse[LAMBHULL], LAMBHULL, 
          inverse[IMAGE[inverse[S]]]], id[fix[IMAGE[inverse[S]]]]] := 
      True

SubstTest[subclass, composite[x, inverse[x]], 
        id[y], {x -> composite[IMAGE[inverse[S]], inverse[LAMBHULL]], 
          y -> fix[IMAGE[inverse[S]]]}] // Reverse

This is our final version:

FUNCTION[composite[IMAGE[inverse[S]], inverse[LAMBHULL]]] := 
      True