-
Notifications
You must be signed in to change notification settings - Fork 88
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
revise df-prjsp #3214
revise df-prjsp #3214
Conversation
This is basically https://us.metamath.org/mpeuni/bj-dfssb2.html (its RHS is df-sb by https://us.metamath.org/mpeuni/dfsb7.html). |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Looks good!
$( | ||
TODO: The proof is that <. a , b , c , ... >. has either a = 0 or a =/= 0. | ||
Since <. 0 , b , c , ... >. .~ <. 0 , nb, nc , ... >., the case a = 0 | ||
corresponds to the (n-1)-dimensional projective space. When a =/= 0, there | ||
is <. a , b , c , ... >. .~ <. 1 , b/a, c/a, ... >. Since the later terms | ||
are irreducible it corresponds to all (n-1)-tuples of ( Base ` K ) which is | ||
equivalent to the construction of an affine space. Note that the closest | ||
definition to affine space so far seems to be ~ df-ehl , which is specific | ||
to reals. | ||
|
||
prjspnf1om1.1 $e |- F = ??? $. | ||
@( A bijection between an n-dimensional projective space and its | ||
(n-1)-dimensional affine and projective spaces. (Contributed by Steven | ||
Nguyen, ??-??-2023.) @) | ||
prjspnf1om1 @p |- ( ( N e. NN /\ K e. DivRing /\ ?? ) -> | ||
F : ( N PrjSpn K ) -1-1-onto-> ( ( K ^m ( 0 ..^ ( N - 1 ) ) ) u. | ||
( ( N - 1 ) PrjSpn K ) ) ) @= | ||
? $. | ||
$) |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
~f1oun
seems to be the best top-level theorem to start with.
Then you can probably explicitly construct the mappings.
@icecream17 left a comment in #3219 , so I think he saw the remarks here, too, and it is safe to merge this pull request. |
Restricts the domain of the equivalence relation to not include 0, to make theorems using the equivalence operator nicer
sidenote: I'm stumped on trying to prove something like:
The reverse direction becomesedit: invalid alrimiv because of $d v condition( x = t -> ph ) /\ y = t /\ E. x ( x = t /\ ph ) -> A. x ( x = y -> ph )
after a simple alrimiv which seems so possible but I can't find a solution???( x = y -> ph )
is easily provable but there's no easy way to add the quantifier.