search

metamath / set.mm

Metamath source file for logic and set theory
Other
253 stars 88 forks source link

Merge developments of R^n #52

Open digama0 opened 8 years ago

digama0 commented 8 years ago

On Thursday, April 7, 2016 at 8:34:08 AM UTC-4, fl wrote:

I think that ( RR ^N ) and ( CC ^ N ) in my mathbox or what is related to euclidean spaces in Madsen's mathbox deserve to be made official.

The version I would prefer to see (personal taste only) is R^n and C^n as Hilbert spaces, meaning the structure product of n copies of RR or CC with an inner product and induced norm. This will allow for reusing structure theorems for groups, vector spaces etc. (which FL's mathbox version doesn't do) and will also allow dealing with the inner product structure (which supercedes JM's definition of the norm).

If you like Madsen's mathbox version, an easy way to get it into main is just to use it in your mathbox. Since mathboxes are independent, any common work will be moved up.

That said, I'd really like to have some theorem that depends essentially on the structure being R^n / C^n to justify the definition. So far it's all statements that apply to all vector spaces or all Hilbert spaces. Madsen's proof that boundedness is equivalent to total boundedness in R^n is a good example, but if it's just the one theorem it is not really worth it.

As you say, we currently have three versions of R^n in the database. The only way this will be moved up is if someone takes it upon themselves to unify all three developments, meaning that a new development (or extension of one of these three) must encompass all the major results of the other two developments.

The Tarskian geometry approach is interesting, but I think your "planar incidence geometry" approach is the better one. Essentially, define the geometry axioms in general and form a new structure for them (and prove what results you can from this structure), then show that R^n has a compatible structure, so that R^n acquires the geometry theorems. (EDIT: I don't mean to suggest here that Aitkin's axioms for planar incidence geometry are better than Tarski's, but rather that we should use the "axiomatic" approach which is not R^n-specific - this applies equally to either axiomatization.)

sorear commented 8 years ago

Side note: df-plig has a broken link, should be http://public.csusm.edu/aitken_html/m410/betweenness.08.pdf

digama0 commented 8 years ago

@sorear Fixed in https://github.com/metamath/set.mm/commit/04f3414a460ea4e8e06ba0167f0cf690a52ebc09.

tirix commented 5 years ago

I think it's worth mentioning in this issue this definition proposed in a post by Mario and another post by Mario df-rrx $a |- RR^ = ( i e. _V |-> ( toCHil ' ( ( ringLMod ' ( CCfld |'s RR ) ) freeLMod i ) ) ) $. df-rrxf $a |- RR^() = ( i e. _V |-> ( ( RR^ ' i ) |'s { f e. ( RR ^m i ) | ( '' f ( _V \ { 0 } ) ) e. Fin } ) ) $. df-prds $a |- Xs_ = ... u. { <. ( .i ' ndx ) , ( f e. v , g e. v |-> ( s gsum ( x e. dom r |-> ( ( f ' x ) ( .i ' ( r ' x ) ) ( g ' x ) ) ) ) ) >. }

tirix commented 5 years ago

The first step, to update ~ df-prds, is done in #931.

The next step, which is not listed above, would be to also update ~ df-sra subringAlg to define its inner product as the ring multiplication. Am I correct?

tirix commented 5 years ago

Second step, with the definition of RR^ and EEhil (to follow the naming convention for structures), is done in #937.

A third step would be to pull-in Jeff Madsen's metric.