[Metamath] Re: Proposal: Allow primed class variables in set.mm body (e.g., A')

['ookami' via Metamath]

Hello David,

(1) How do you expect this to be clearly distinctive from df-fv? (2) There 
are numerous write styles in use for all kind of mathematical classes, e.g. 
I've seen German Fraktur for topological spaces. I think your proposal 
opens up a can of worms,in the end, once an exception is tolerated.

I am not sure whether your idea really works this way. One should implement 
a translator that produces adapted output on the web sites only, to 
accomodate to common styles in particular fields of mathematics.

Wolf

David A. Wheeler schrieb am Sonntag, 12. Juli 2020 um 22:03:28 UTC+2:

> I propose that we allow A' , B' , etc., as class variables, at least to 
> support geometry.
> This would make it much easier to indicate corresponding values (such as 
> points)
> and make it easier for proofs to more obviously match their original 
> source material.
> Having primed variables is already common mathematical practice, so we'd be
> supporting common practices.
>
> Background:
> I'm hoping to contribute to the Elementary Geometry section, so I've been 
> walking through
> the current set.mm work due mostly to Thierry Arnoux, Mario Carneiro, and 
> Scott Fenton.
> This involves reading [Schwabauser], something of a trick since it's in 
> German and
> I can't read German. (Hello Google translate!)
>
> An unnecessary challenge in doing this is that the geometry proofs
> often involve many points that correspond to each other, which is 
> typically indicated by
> a prime. However, the set.mm main body doesn't support that. This 
> inability to easily indicate
> point correspondences makes it unnecessarily hard to read the proof 
> statements, AND
> it creates an unnecessary difference between set.mm and the original 
> source material.
>
> For example, here are the key hypotheses and conclusion of
> http://us.metamath.org/mpeuni/tgifscgr.html
>
> 𝐵 ∈ (𝐴𝐼𝐶) ; "B is between A and C"
> 𝐹 ∈ (𝐸𝐼𝐾))
> (𝐴 − 𝐶) = (𝐸 − 𝐾)
> (𝐵 − 𝐶) = (𝐹 − 𝐾)
> (𝐴 − 𝐷) = (𝐸 − 𝐻)
> (𝐶 − 𝐷) = (𝐾 − 𝐻)
> Proves
> (𝐵 − 𝐷) = (𝐹 − 𝐻)
>
> If we allowed A' etc., this could expressed as the following, which
> is MUCH clearer because the "primed" class variables make
> correspondences MUCH more obvious:
>
> 𝐵 ∈ (𝐴𝐼𝐶) ; "B is between A and C"
> 𝐵' ∈ (𝐴' 𝐼 𝐶' )
> (𝐴 − 𝐶) = (𝐴' − 𝐶' )
> (𝐵 − 𝐶) = (𝐵' − 𝐶' )
> (𝐴 − 𝐷) = (𝐴' − 𝐷' )
> (𝐶 − 𝐷) = (𝐶' − 𝐷' )
> Proves
> (𝐵 − 𝐷) = (𝐵' − 𝐷')
>
> Having "primed" variables is very common in mathematics, and
> there's no technical reason set.mm can't support them.
> These are *already* defined in the Mathbox for Jonathan Ben-Naim, so they
> just have to be moved up. We could also move up double-primed (A") if 
> desired.
>
> Let's do it!
>
> --- David A. Wheeler
>

-- 
You received this message because you are subscribed to the Google Groups 
"Metamath" group.
To unsubscribe from this group and stop receiving emails from it, send an email 
to metamath+unsubscr...@googlegroups.com.
To view this discussion on the web visit 
https://groups.google.com/d/msgid/metamath/a67ca28d-aa9b-4fb0-80df-f58935775628n%40googlegroups.com.