On Tuesday, June 4, 2019 at 11:15:03 AM UTC+2, Jon P wrote:
>
> Benoit I like your way of using barycentric coordinates to express the
> interior of the triangle, that is quite elegant. I am not sure how to fit
> it into this scheme though,
>
The points "inside" the tr
x A $. $d x ps $. sbcie.1 $e |- A e. _V $.
sbcie.2 $e |- ( x = A -> ( ph <-> ps ) ) $.
sbcie $p |- ( [. A / x ]. ph <-> ps ) $=
Benoit
>
> My experience is that implicit substitution is more easy to work with.
> _
> Thierry
>
>
>
--
You received this
The ideal solution would be to use MetaPost to design a real $\Aleph_0$...
or maybe to use an existing one (see
https://tex.stackexchange.com/questions/170476/how-to-get-aleph-and-beth-symbols-in-similar-font#170494
for various fonts) ?
Benoit
--
You received this message because you
On Tuesday, May 28, 2019 at 9:25:47 PM UTC+2, Giovanni Mascellani wrote:
>
> Hi! I think there is a general trick to replace a $d x A or $d x ph$
> condition in a theorem with the corresponding F/_ x A or F/ x ph, but I
> do not remember it. Can anybody help me?
>
> (in this specific case, I
Using the replacements I gave above yielded the proof:
${
$d z A $. $d x y z $. $d z ph $.
sbcex2f.1 $e |- F/_ x A $.
$( Move existential quantifier in and out of class substitution.
(Contributed by NM, 21-May-2004.) (Revised by NM, 18-Aug-2018.) $)
sbcex2f $p |- ( [.
Sorry, I misread Mario's post. It looks like we agree on F/2 from an
intuitionitic point of view. Then why not take the same definition for
set.mm ?
In any case, I will not do this right now and I would first write a draft
in my mathbox before making any change.
--
You received this message
On Tuesday, May 28, 2019 at 6:02:38 PM UTC+2, Mario Carneiro wrote:
>
> I'm okay with the alternative df-bj-nf definition. If the use of the
> definition E. is undesirable, here are some more alternatives:
>
> $a |- ( F/1 x ph <-> A. x ( ph -> A. x ph ) )
> $a |- ( F/2 x ph <-> ( E. x ph -> A. x
.
I'll be interested in your comments, especially on adopting the alternate
definition for non-freeness.
Benoit
--
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
| \exists a, b, c \in
\R_{\geq 0}, a + b + c = 1 and X = a A + b B + c C \}
This generalizes to all simplices in any dimension (starting with dimension
0).
By the way, I think that in your (Thierry) description, you got the
opposite sign for F and your S is actually a parallelogram.
Benoi
Maybe you can also begin a new thread, with a subject like "Area of a
triangle".
Thanks,
Benoit
--
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
age like Metamath)
I think that it is often possible to avoid "[ / ]-substitutions" (are they
the ones called "implicit substitutions"?) by modifying your proof a bit,
and use "explicit substitution" instead (typically with steps like "x = A
-> ( ph <-> ps )").
like exponential time
complexity in the number of $e-hypotheses of the theorem to minimize with,
and 4syl has four $e-hypotheses...
I agree that it is a useful theorem, but you can see manually if it is
worth to launch a "minimize 4syl/override": if your proof already uses 3syl
and
lt;. x , y >. | ( <. x , y >. e. A /\ y e. C ) }
> !qed::|- B e. dom area
>
> It looks false: what if C is not measurable ? (e.g. take A to be the unit
square and C a non-measurable subset of [0,1])
> Also, why not try directly with the deduction version th
At
least, do a line break after "$=". Never use tabulations. If the line of
the statement needs to be broken, then break it after operators which are
"high in the parsing tree" (I don't know how to say it precisely and
concisely, but you see what I mean).
Benoit
--
, reflections), so that you can then suppose that your triangle
has one vertex at (0, 0), one at (a, 0) with a > 0, and the third at (b, c)
with c > 0, and then its area is ac/2. Obviously, the invariance under
displacements is much harder to prove, but this is the correct way to go.
Beno
. So go directly for
the deduction form (unless the proof is short enough that you can prove the
closed form). I think you can state more general rules like the one you
wrote. For arearect and areaquad, I would say: wait until you need the
deduction form.
Benoit
--
You received this mess
} = { z | E. x E. w ( z = <. x , w >. /\ [ w / x
] x = 2 ) }
which yields, if I'm not mistaken,
|- { <. x , x >. | x = 2 } = { z | E. x z = <. x , 2 >. }
which is clearly false.
Benoit
--
You received this message because you are subscribed to the Google Groups
&quo
which imply that { <. x , x >. | ph } is not a subset of the diagonal,
would be going too far away from mathematical practice.
Benoit
--
You received this message because you are subscribed to the Google Groups
"Metamath" group.
To unsubscribe from this group and stop receiving email
, but not on
a direct product.
As for the unicode symbol for the direct sum of copies of \R, I would use
Mario's suggestion from a previous thread, i.e. R^() instead of R^. This
would free up the symbol R^ to be used for the direct product.
Benoit
--
You received this message because you are subscribed
I mentionned it in
https://groups.google.com/d/msg/metamath/BSOOYEw2sjU/TmHaccI5AwAJ and I
think Thierry took it into account in his treatment (he was part of that
discussion in the fall).
Benoit
On Thursday, June 27, 2019 at 3:24:45 PM UTC+2, David A. Wheeler wrote:
>
> The paper &quo
t;
part, since it is in the Metamath book, where it belongs, and wikipedia is
not a "how to" nor a substitute to the Metamath website or book.
* Other sections
Benoit
On Friday, July 12, 2019 at 9:18:20 AM UTC+2, Jon P wrote:
>
> It looks like they have a s
the unity of mathematic (no 's'!). I've read big
chunks of the first five books and "Lie groups and algebras" and spectral
theory. It is a reference book, not a textbook or a pedagogical device.
Benoit
--
You received this message because you are subscribed to the Google Grou
ect is dormant, on its way, soon to be resurrected...
Benoit
On Sunday, July 14, 2019 at 2:48:08 PM UTC+2, fl wrote:
>
>
> > or belonging to the sphere of influence of Germany (Banach)
>
> I have just noticed that Banach wrote in French in Polish reviews. So much
> for the G
(or even searching with ctrl+F in a
text editor)? I guess this is doable in mmj2 with regular expressions?
I've been a bit extreme in not overloading symbols, and defined couples of
classes as (| A ,, B |) (see bj-c2uple), although the unicode symbol for
",," is "," so tha
sponding STIX version. I'm not sure whether it is
font-family: STIX2Math;
src: url(STIX2Math.woff2);
or a variant (e.g. STIXTwoMath). Then, we could easily compare ascii.html
with ascii-STIX.html from several browsers, devices, etc. before switching.
Benoit
--
You received this message b
es "text-only") than go into very intricate hard-to-maintain
code in order to have a better looking symbol.
Benoit
--
You received this message because you are subscribed to the Google Groups
"Metamath" group.
To unsubscribe from this group and stop receiving emails from
mpler statements, both the
curried and the uncurried forms should be in set.mm. But later? Is there
a "good practice", a rule of thumb?
Thanks,
Benoit
--
You received this message because you are subscribed to the Google Groups
"Metamath" group.
To unsubscribe from this group and st
is not
concerned with bidirectional writing).
See the STIX font project: https://github.com/stipub/stixfonts
A comparison of STIX and XITS, dated from before STIX 2, but anticipating
it: https://tex.stackexchange.com/questions/227216/stix-versus-xits
Benoit
--
You received this message because you
c-statements? i.e. have
blocks
$c smurf $.
csmurf $a class smurf $.
df-smurf $a smurf = ... $.
This would look more systematic. As suggested above, maybe one could also
standardize the comments, for example "Extend class notation to smurf /
Syntax for smurf / Define smurf, the function t
s as
well. In my case, I haven't tried to be systematic and haven't thought too
much about the most economical way to treat these, but I used some of them
to prove a formula for barycentric coordinates in ~bj-bary1.
Benoit
--
You received this message because you are subscribed to the Goo
e, I think it would at least be possible that the "us" version never
be the latest: when doing the update, first copy "us2" to "us", and then
update "us2".
Benoit
--
You received this message because you are subscribed to the Google Groups
"Metamath&qu
y (with travis?) that if a PR contains
proof modifications, then these modifications do not add new dependencies
on $a-statements? (You can see the same obsession that led me to suggest
the modification of "minimize_with" to default to "no_new_axioms".)
Benoit
--
You rec
r (PR
#1068). In PR #1072, I added a comment to ex-natded5.3i to recommend use
of jccir instead. I also removed the two remaining uses of ex-natded*
theorems mentioned by Alexander.
Benoit
--
You received this message because you are subscribed to the Google Groups
"Metamath" group.
To
I obtained 40
characters (uninteresting: simply add an unrelated $v-statement to the
previous ones). For "containing a correct proof and an $f-statement", I
obtained 44 characters.)
Benoit
--
You received this message because you are subscribed to the Google Groups
"Metamath&qu
old.
Can the "updating schedule" for both servers be documented somewhere?
Thanks,
Benoit
On Wednesday, August 21, 2019 at 8:47:32 AM UTC+2, Alexander van der Vekens
wrote:
>
> Considering Norm's explanations, I think a delay of at most 3 days would
> be OK. This should also be enough
to detect the
modifications that are in between a "$=" and a "$." and return the
associated label (which is the word immediately preceding the "$p"
immediately preceding that "$="). I'm not asking that it be implemented
(though if someone feels like i
Alexander, can you check, using the script "scripts/min.cmd", whether the
theorem "jccil" (where the conclusion is "( ph -> ( ch /\ ps ) )" ) is also
worth adding?
Thanks,
Benoit
On Wednesday, August 21, 2019 at 12:52:29 AM UTC+2, Norman Megill wrote:
>
>
equence A(n) does not converge, so the space is not
complete."
[Proof: Let B be in ( RR^() ` NN ). Therefore, B \in span(e_1, ..., e_k)
for some k. Therefore, for arbitrarily large n (indeed, for all n larger
than k), on has |A(n) - B| > 1/(k+1). So A(n) does not converge to B. Since
B w
directory of the mm file with
respect to that of the metamath program in the RunParms.txt file ? E.g.
LoadFile,../../git/set.mm/set.mm
Thanks,
Benoit
--
You received this message because you are subscribed to the Google Groups
"Metamath" group.
To unsubscribe from this group and s
Thanks for the detailed explanations.
Concerning weaker arithmetics: Is EFA the same thing as I\Delta_0 + exp ?
And if I understand correctly, you say that I\Delta_0 should actually
suffice ? Or maybe I\Delta_0 + \Omega_1 ? (Of course, I think PA was a
wise choice for a first attempt, for
finitional soundness
check. Dummy variables [y] are possibly free in the definiendum, and no
justification is available.
---
[By the way: the failure to pass the test for df-clab, df-cleq, df-clel
should not be due to the obsolete axioms mentioned, but this is another
matter.]
Benoit
--
You r
ly, any non-setvar dummy variable could be replaced by
_V (or (/)) or T. (or F.) depending on their type.
Benoit
--
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
Hi David,
I think my GitHub avatar was automatically generated. You may use it for
the Gource visualization.
Thanks,
Benoît
--
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
umo0 which are backups of
demoted theorems placed in my mathbox.)
Benoit
--
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...@googl
of a section would be that of its first statement)?
Benoit
--
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
ery useful. It is always open on my desktop when I work on set.mm.
Benoit
--
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...@googl
ibuting.md file on the
mmset.html page (I'll make a proposal in my next PR). Note that the
Metamath home page has a FAQ section with a question "How can I contribute
to Metamath", and the answer has a link to github.com/metamath/set.mm .
Granted, this is not very direct.
Benoit
--
hen I generate the html pages on my computer, the characters look fine.
This might be because the fonts are not installed by default?
Remark: actually, I generally use in \widehat{A} instead of \hat{A} (and
similarly \overline{A} instead of \bar{A}) since I think the larger marks
look better, but I ha
not work on metamath.org where, if
I understood correctly, a special set of fonts is loaded locally?
Benoit
--
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, sen
> Therefore, I still would propose to recommend to use the form $e |- ( ( ph /\
> x = ... ) -> ... ) $. in deduction style.
I agree. Plus, this is more systematic hence easier to remember.
> Already existing theorems need not to be rewritten
They need not but they could !
> (by the way, many
Thanks. Indeed, with this extended definition of left/right-associativity
(that is, associativity among all operators of a given precedence, and not
merely associativity of a given operator), it all makes sense and is
consistent, and indeed the condition given by Mario to ensure unambiguity
b * c" is to be read as
"( a * b ) * c", and nothing more than that. It seems that to you, there
is an additional meaning: if * and + have the same precedence and are both
left-associative, then " a * b + c " is to be read as " ( a * b ) + c". It
seems a bit abu
I hope parts of this discussion will make their way into some kind of
documentation, in particular the possibility to add extra parentheses and
the fact that MM0 uses the term "sort" instead of "type" because the type
system is voluntarily poor, and if some type theory is to be implemented,
Thanks for the clear explanations. I didn't know this use of the word
"barb", and I see on dictionary.com "unpleasant remark". My remarks were
certainly not meant to be unpleasant, and I'm interested in seeing where
MM0 goes.
Is it always possible to put parentheses, even where they are not
Thanks Giovanni. I hope Mario can also chime in on the questions in my
previous message, since these are not right-or-wrong issues, but are more
about balancing pros (proximity with mathematical practice) and cons (more
complex parser).
You write:
> In you example, you definitely want "." to
Hi,
If I recall correctly, the us2 server is updated within 24 hours of a new
merge in metamath/set.mm on github (I cannot retrieve this information).
But the merge https://github.com/metamath/set.mm/pull/1261#event-2813593206
is from 20 nov. 2019 à 02:26 UTC+1 (35 hours ago at the time of
I'm also hoping for an outline of the proofs (especially the "encoding" in
set.mm and the difficulties encountered). Is there a particular reason why
sin, cos were used instead of exp ?
Benoît
--
You received this message because you are subscribed to the Google Groups
"Metamath" group.
To
Thanks Glauco for this outline.
First, I re-ask my previous question: is there a particular reason you
chose sine and cosine over the exponential function ?
Like FL, I think several lemmas deserve to be in the main part. I will use
your sectioning:
ORDERING ON REAL NUMBERS - REAL AND
>
> The basic idea is to run 'minimize */a */n ax-*' on each proof and send
> the results (in a log file) to me, without saving the proof.
>
Maybe add the options /VERBOSE /TIME to have all the information possible.
Benoît
--
You received this message because you are subscribed to the Google
Alexander,
I'm looking at the section comment of "21.25.10.3 The Cayley-Hamilton
theorem". What is the metamath label corresponding to Equation (2) ? I
see that ~cramer has no theorem referencing it. I thought the natural
proof of (2) would use Cramer's rule ?
Thanks,
Benoît
--
You
On Sunday, October 6, 2019 at 12:50:37 AM UTC+2, Mario Carneiro wrote:
>
> It can also be used together with bitwise type logical operations, such as
> df-cad and df-had.
>
To give an example, I added http://us.metamath.org/mpeuni/bj-cadif.html
bj-cadif|- (cadd ( ph , ps , ch ) <-> if- (
Indeed, it totally makes sense.
Thanks.
Benoit
--
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
Prompted by the post on the proof of convergence of Fourier series, I
looked at other "100" theorems and stumbled on the Stone-Weierstrass
theorem.
~stowei has a dv condition on F,t. This appears to imply that stowei shows
only approximability of constant functions. Similarly, ~stoweid has
>
> the proofs that I followed stated the coefficients in terms of sine and
> cosine. Some of them, then, proved some intermediate results using the
> complex exponential form (it simplified some integral calculation), some
> other sources instead kept using sine and cosine everywhere. When I
Now that it's back to normal, I have two naive questions:
1) Isn't the purpose of mirror sites to serve as replacements when an even
like this occurs ? However, during the event, it seems the mirror sites
were unavailble either. Can we do something about it ?
2) Because of the event, the
Just in case this wasn't clear enough: these were two naive questions, as I
wrote. Maybe I should have written "genuinely naive" or "naively genuine"
to be clearer. Anyway, thanks Norm for the explanations.
Benoît
On Thursday, October 24, 2019 at 10:42:11 PM UTC+2, vvs wrote:
>
> BTW, there
Actually, I would go for the biconditional, as Mario suggests, since it's
always nicer to have a characterization. The useful part is indeed the
forward implication, since the reverse implication is always true and
obvious and easy to prove, but I think this is not a reason to keep it out
of
Hi Mario,
That's a very nicely written paper, that shows some impressive work! It
made me want to try and learn mm0. I'll have to digest your article more.
I found some typos after a first reading (maybe for some of them, it is
actually me misunderstanding the paper):
p.4b: \bar y \sharp \bar
Hi all,
A few months ago, after the discussion here on bundling with Mario, I
experimented removing dependencies on ax-13 from many theorems. This is in
my mathbox, in the section titled
21.29.4.12 Removing dependencies on ax-13 (and ax-11)
(beginning with
Thanks for your suggestions. In any case, I do not plan to move anything
to the main part before the end of 2019, so we still have time to discuss.
As for Jim's remarks: in your specific example, sb56 currently requires
ax-13, whereas bj-equs5v (and bj-sb56) do not. But I see a shorter way to
As for definitions: it looks like Alexander was referring mainly to
$e-statements which serve the purpose of local definitions, while David
talked mainly about the $a-statements. As for the $e-statement
definitions, they can serve as definitions used in the statement of the
theorem, or only
A word of caution (without being dismissive whatsoever of Wolf's great
work): shorter proof (or, more precisely, proof with fewer steps) does not
always mean simpler proof, or easier-to-understand proof. This is why I am
thankful that Wolf keeps *OLD versions (which should be checked before
On Thursday, November 28, 2019 at 2:18:19 PM UTC+1, ookami wrote:
>
> The rules by which a proof is considered shorter were explained to me by
> Norm about 10 years ago: First look at the size of the encoding of the
> compressed proof, not taking the references into account. On tie, count the
>
Hi all,
A few months ago, I added the "conditional operator for propositions" to my
mathbox (currently Section 21.29.1.6, beginning at
http://us2.metamath.org/mpeuni/wif.html). I propose to move it to the main
part for the following reasons:
* it is a pretty natural operator
* it is analogous
Looks great !
Maybe moving the captions lower-left (instead of lower-center) would make
both the captions and the graph more legible (the captions, because they
would be left-aligned, and the graph, because it would be less obstructed
by the captions).
It's a bit strange that at around 0:01,
>
> (Actually df-v is an exception; it should probably read { x | T. } and I
> guess the use of x = x is a historical accident?)
>
This has been proposed in
https://groups.google.com/d/msg/metamath/V3jmbWUd_mM/RAk2DEA3FQAJ, with
explanations that I still stand by. With the new definition
Hi David,
I agree with Alexander that the paragraph "Unlike the Gource...
improvements" can be removed (and the older video it mentions can be
removed too, if youtube allows that).
Concerning the following paragraph, I would shorten it to something like:
The initial "big bang" effect is due
>
> 0. Thanks to Benoit Jubin for applying the rubric at the top of
> CONTRIBUTING.md which enhances the instructions in
> https://github.com/metamath/set.mm/wiki/Getting-started-with-contributing
> <https://www.google.com/url?q=https%3A%2F%2Fgithub.com%2Fmetamath%2Fset.m
David: yes, ~bisymOLD and ~bi3antOLD should have both discouragement tags.
I'm away from my main computer... can you add them ?
Actually, most *OLD and *ALT should probably have both discouragement tags
as well, it seems ?
Thanks,
Benoît
On Thursday, February 13, 2020 at 9:13:39 AM UTC+1,
>
> I started my quest towards IMO 1972 B2 by formalizing a simple
> induction problem (just for fun): `( N e. NN -> 3 || ( ( 4 ^ N ) + 5 )
I think ~ inductionexd (with the caveat below) is a nice instructive
example, and could be moved to main, as the first theorem of the new
subsection
Stan: you're right about the need to prove this (if using explicit
substitution): look for the utility theorems exchanging [. / ]. with other
symbols (quantifiers, operations). As said by Jim and Thierry, who are
more experienced in proof building, implicit substitution might be easier
to
> One question for which I'm looking guidance is on using quantifiers or
not.
That's a very important question, and I hope someone with more experience
will be able to shed some insight. In particular, if one has a hypothesis,
say, "E. x ph", then it is common to see in textbooks things like
Another proof I just found (sorry, it's not about the formalization):
Let x be such that f(x) \neq 0 and let y \in \R. Set a = g(y).
Set u_n = f(x + ny) for n \in \Z. It satisfies the linear recurrence
relation u_{n+2} = 2a u_{n+1} - u_n. The characteristic relation is r^2 -
2ar + 1 = 0. The
>
> I have stumbled upon the supremum definition but it looks more intricate
> to use than a manually defining it inline on the real line (unless you’re
> referring to another definition of the least upper bound). That’s precisely
> one of the open questions I have about how to go about
Here is a question prompted by my remark in
https://groups.google.com/d/msg/metamath/Nvh_ue-PSBM/Nj-XpBvBAAAJ
"there is some gymnastic to do to put things in the right "slot", which
looks painful..."
I see in ~df-cat that if c is a category, then ( Base " c ) is actually the
set of objects
Ok. I'm not insisting since I'm not fond of extensible structures anyway.
But it is certainly not odd to make morphisms the underlying set of a
category. The fact that an "arrows only" definition of a category is
possible shows that it's that latter set which is more important. Also, it
is
On Saturday, February 1, 2020 at 3:37:57 AM UTC+1, Norman Megill wrote:
>
> On Friday, January 31, 2020 at 8:23:08 PM UTC-5, Benoit wrote:
>>
>> Regarding the possible introduction in the main part of semigroups and
>> magmas:
>> When I look at the page http://us2.m
To answer FL's latest message: the first and foremost thing that Norm has
done and still does for us is having created the Metamath language,
continuously improving the Metamath C program (the "official
implementation" of the Metamath language), and having begun and still being
the main
Regarding the possible introduction in the main part of semigroups and
magmas:
When I look at the page http://us2.metamath.org/mpeuni/df-mnd.html I feel a
bit dizzy. The abundance of parentheses and conjunctions makes it hard to
parse. Did you notice that the clause stating closedness is
Thanks David. I looked at the corresponding MPE webpage
(http://us2.metamath.org/mpeuni/mmtheorems21.html) and the following, and
indeed
aevALT
ax16nfALT
dral1ALT
dveeq2ALT
sbequ8ALT
equsb3ALT
should have the "(Proof modification is discouraged.)" tag. They already,
and correctly, have the
I think that the *ALT and *OLD theorems appearing in the list (and those I
quoted earlier in this thread) can be given both discouragement tags. This
will take care of most of "my" cases (and others). I can do it if Norm
wants. As for the other minimizations of theorems of the form bj-* in
>
> Yes, ~hashssle is a specialization of ~hashss and could be replaced (and
> removed afterwards). ~hashssle (and ~bj-abf), however, are in mathboxes. In
> my opinion, the owners of the mathboxes should be responsible for cleaning
> up such cases. But it would be great if a list of such cases
On Thursday, February 13, 2020 at 5:46:36 PM UTC+1, Mario Carneiro wrote:
>
> That said, I think it would still be better to move all definitions needed
> for df-prds before it. This is a downside of the "everything structure"
> approach, but it does not displace too many definitions. We can
On Friday, January 10, 2020 at 1:52:20 AM UTC+1, Mario Carneiro wrote:
>
> we should have guarded the application to avoid seeing it in the first
> place.
>
How would you do that ? (I gave some ideas some time ago on this group, but
the drawbacks were deemed to outweigh the benefits.)
Thanks,
As promised at the end of
https://groups.google.com/d/topic/metamath/yzQnexbXv-8/discussion , I'm
going to list a few ways I can think of to avoid "nonsensical", or "junk"
theorems in set.mm. This is not a proposal to change anything in set.mm,
at least for the moment. The only aim of this
On Saturday, January 11, 2020 at 1:52:55 PM UTC+1, fl wrote:
>
> Someone suggested using Bourbaki as a guide for ordering the definitions
> and theories related to structures. I think this is a good idea.
> It is the longest and most comprehensive treatise on structures.
>
You probably refer to
Thanks. Yes, Mario's and David's suggestions are two possibilities I had
in mind, with other, more strict ones, with the drawbacks alluded to
above. I'll try to list them in a separate thread.
Benoît
--
You received this message because you are subscribed to the Google Groups
"Metamath"
On Saturday, January 11, 2020 at 10:44:31 PM UTC+1, Mario Carneiro wrote:
>
> qed::foo |- ( T. -> RH )
>
I don't understand: it looks like you are using foo with the substitutions
ph <- T. and THM <- RH, but in order to make the latter substitution, you
need to prove that RH has type |- , which
This was proposed in PR #1105. There is an ensuing discussion.
Benoît
--
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
unday, January 12, 2020 at 6:09:52 PM UTC-5, Norman Megill wrote:
>>
>> On Sunday, January 12, 2020 at 5:24:59 PM UTC-5, Benoit wrote:
>>>
>>> On Saturday, January 11, 2020 at 10:44:31 PM UTC+1, Mario Carneiro wrote:
>>>
>>
>> ...
>>
>
1 - 100 of 283 matches
Mail list logo
