HomePage RecentChanges

raph

I've been hacking on metamath and my own variant of it, Ghilbert.

My main blog is at: http://advogato.org/person/raph/

Hi Raph, I have seen you are working on continuous functions. What are your projects about it ? I ask it because I have two theorems concerning the continuity of ( f o. g ) when f and g are continuous (or continuous at a point) in my task list and I prefer to avoid the frustration of seeing your proofs published just when I finish mines ? If you want to deal with them, tell me and I will change for something else. – 22-Nov-2006 fl

Hi Frederic, it is very good that you ask this question. I asked Norm about a month ago for some topology theorems, and he assigned cnsscnp, cncnp, and metcn (below). As you can see from mmrecent, I just finished the second one of these.

  ${
    metcn.1 $e |- X = ( 1st ` M ) $.
    metcn.2 $e |- C = ( 2nd ` M ) $.
    metcn.3 $e |- Y = ( 1st ` N ) $.
    metcn.4 $e |- D = ( 2nd ` N ) $.
    $( Two ways to say a mapping from metric space ` M ` to metric space ` N `
       is continuous.  Theorem 1.3-4 of [Kreyszig] p. 20.  The second
       biconditional argument says that for every positive "epsilon" ` y `
       there is a positive "delta" ` 0 < z ` such that a distance in ` M `
       less than delta maps to a distance in ` N ` less than epsilon. $)
    metcn $p |- ( ( M e. Met /\ N e. Met ) ->
                ( F e. ( ( open ` M ) Cn ( open ` N ) ) <-> ( F : X --> Y /\
                A. x e. X A. y e. RR ( 0 < y -> E. z e. RR ( 0 < z /\
      A. w e. X ( ( x C w ) < z -> ( ( F ` x ) D ( F ` w ) ) < y ) ) ) ) ) ) $=
                      ? $.
  $}

After I prove metcn, I will probably go on to do other Ghilbert things. I wanted serious theorems in the set.mm universe to test out my interactive math typesetting GUI (see screenshot on the Ghilbert application page). So far the experience has been quite positive. As for the specific question of composition of continuous functions, I would probably find those fairly easy to prove now, but I'm perfectly happy to leave those assigned to you if you think you will enjoy them.

The more this becomes a collaborative project, the more need there is for coordination, both to avoid duplicated work and so that the people working can share tips, knowledge, etc. I'm not sure whether this wiki space is appropriate, whether a wiki page for each theorem in progress would be spammish, but ultimately I think something like that is needed. – raph

OK thank you Raph. So I'll go on with the continuity of ( f o. g ) unless Norm disagrees. – fl