Thank you for the pointer, Mario. Is this negative vs. positive position
terminology something you neologized on the fly? Or does it have precedent? If
I'm grokking you correctly, the positive positions plug into the negative
positions, which jibes with your explanation and the Is-a-set convention
This has been bugging me midly for a while, but I couldn't figure out what the
Fr symbol in df-fr stood for:
19201 df-fr $a |- ( R Fr A <-> A. x ( ( x C_ A /\ x =/= (/) ) -> E. y e. x
A. z e. x -. z R y ) ) $.
I finally bothered to look up the Takeuti and Zaring reference, which also uses
The A e. V antecedent is confusing me. Might I ask for a quick pointer?
85195 indistopon $p |- ( A e. V -> { (/) , A } e. ( TopOn ` A ) ) $= ... $.
It looks suspiciously close to A e. _V which reas as "A is a set", but in this
case the V is just floating. What are the semantics here?
--
Here are some brainstorming questions and thoughts:
Would it make sense to have "search path" variables for metamath and mmj2?
The FHS describes /var/lib and /var/local/lib as places for "variable data"
associated with programs in /usr and /usr/local, respectively. Ostensibly,
the purpose of
Thank you for starting this discussion. As a package manager, I certainly
empathsize strongly with efforts to make the current installation more
standards-compliant. In that vein, I would recommend against defaulting to
$HOME installations. Programs which do this are not common, play badly with
Excellent. So I just happened to stumble upon a nice method used to organize
related deductions. Much appreciated.
On Fri, Oct 25, 2019 at 06:24:40AM -0700, Jim Kingdon wrote:
> This is relatively common when people want related theorems to have the same
> hypothesis.
>
> If you look at set.mm,
