metamath  

Messages by Date

• 2022/01/20 Re: [Metamath] pet $p |- ( ( R (x) ( `' _E |` A ) ) Part A <-> ,~ ( R (x) ( `' _E |` A ) ) ErALTV A ) Partition-Equivalence Theorem with general ` R ` Mázsa Péter
• 2022/01/19 Re: [Metamath] pet $p |- ( ( R (x) ( `' _E |` A ) ) Part A <-> ,~ ( R (x) ( `' _E |` A ) ) ErALTV A ) Partition-Equivalence Theorem with general ` R ` Thierry Arnoux
• 2022/01/18 Re: [Metamath] us2.metamath.org regenerated! Let me know ASAP of any serious problems Benoit
• 2022/01/18 Re: [Metamath] us2.metamath.org regenerated! Let me know ASAP of any serious problems David A. Wheeler
• 2022/01/18 [Metamath] Re: us2.metamath.org regenerated! Let me know ASAP of any serious problems 'Alexander van der Vekens' via Metamath
• 2022/01/18 [Metamath] Re: us2.metamath.org regenerated! Let me know ASAP of any serious problems 'Alexander van der Vekens' via Metamath
• 2022/01/18 [Metamath] us2.metamath.org regenerated! Let me know ASAP of any serious problems David A. Wheeler
• 2022/01/18 Re: [Metamath] pet $p |- ( ( R (x) ( `' _E |` A ) ) Part A <-> ,~ ( R (x) ( `' _E |` A ) ) ErALTV A ) Partition-Equivalence Theorem with general ` R ` Mázsa Péter
• 2022/01/17 Re: [Metamath] Big progress on metamath.org and us2.metamath.org David A. Wheeler
• 2022/01/17 Re: [Metamath] Big progress on metamath.org and us2.metamath.org Jim Kingdon
• 2022/01/17 [Metamath] Re: Big progress on metamath.org and us2.metamath.org Glauco
• 2022/01/17 [Metamath] Big progress on metamath.org and us2.metamath.org David A. Wheeler
• 2022/01/17 Re: [Metamath] pet $p |- ( ( R (x) ( `' _E |` A ) ) Part A <-> ,~ ( R (x) ( `' _E |` A ) ) ErALTV A ) Partition-Equivalence Theorem with general ` R ` Jim Kingdon
• 2022/01/15 Re: [Metamath] Re: Metamath website 'Alexander van der Vekens' via Metamath
• 2022/01/14 Re: [Metamath] Re: Metamath website 'Alexander van der Vekens' via Metamath
• 2022/01/14 Re: [Metamath] Re: Metamath website Benoit
• 2022/01/13 Re: [Metamath] Re: Metamath website 'Alexander van der Vekens' via Metamath
• 2022/01/13 Re: [Metamath] Re: Metamath website Thierry Arnoux
• 2022/01/13 Re: [Metamath] Re: Metamath website Jim Kingdon
• 2022/01/13 Re: [Metamath] Re: Metamath website 'Alexander van der Vekens' via Metamath
• 2022/01/12 Re: [Metamath] Re: Metamath website Benoit
• 2022/01/12 Re: [Metamath] Re: Metamath website Thierry Arnoux
• 2022/01/12 [Metamath] Re: Metamath website Benoit
• 2022/01/12 [Metamath] Re: Metamath website Glauco
• 2022/01/12 Re: [Metamath] Metamath website Thierry Arnoux
• 2022/01/12 Re: [Metamath] Metamath website Scott Fenton
• 2022/01/12 Re: [Metamath] Metamath website David A. Wheeler
• 2022/01/11 [Metamath] Metamath website Thierry Arnoux
• 2022/01/11 Re: [Metamath] Re: Additional Metamath 100 proof in iset.mm: Bézout's identity Jim Kingdon
• 2022/01/11 Re: [Metamath] Re: Additional Metamath 100 proof in iset.mm: Bézout's identity Benoit
• 2022/01/11 Re: [Metamath] Re: Additional Metamath 100 proof in iset.mm: Bézout's identity Jim Kingdon
• 2022/01/11 [Metamath] Re: Additional Metamath 100 proof in iset.mm: Bézout's identity Benoit
• 2022/01/09 [Metamath] Additional Metamath 100 proof in iset.mm: Bézout's identity Jim Kingdon
• 2022/01/08 [Metamath] Re: Conversation between Stephen Wolfram, Norman Megill and Mario Carneiro Benoit
• 2022/01/08 [Metamath] Conversation between Stephen Wolfram, Norman Megill and Mario Carneiro savask
• 2022/01/06 Re: [Metamath] does "standard" theory assume |- -. +oo e. CC ? Thierry Arnoux
• 2022/01/06 Re: [Metamath] Proper Substitution: df-sb & df-sbc Glauco
• 2022/01/06 Re: [Metamath] does "standard" theory assume |- -. +oo e. CC ? Benoit
• 2022/01/06 Re: [Metamath] does "standard" theory assume |- -. +oo e. CC ? Glauco
• 2022/01/06 Re: [Metamath] does "standard" theory assume |- -. +oo e. CC ? Benoit
• 2022/01/05 Re: [Metamath] does "standard" theory assume |- -. +oo e. CC ? Thierry Arnoux
• 2022/01/05 Re: [Metamath] does "standard" theory assume |- -. +oo e. CC ? Benoit
• 2022/01/05 Re: [Metamath] does "standard" theory assume |- -. +oo e. CC ? 'Alexander van der Vekens' via Metamath
• 2022/01/05 Re: [Metamath] does "standard" theory assume |- -. +oo e. CC ? 'Alexander van der Vekens' via Metamath
• 2022/01/05 Re: [Metamath] does "standard" theory assume |- -. +oo e. CC ? Glauco
• 2022/01/05 Re: [Metamath] does "standard" theory assume |- -. +oo e. CC ? Jim Kingdon
• 2022/01/05 [Metamath] does "standard" theory assume |- -. +oo e. CC ? Glauco
• 2022/01/05 Re: [Metamath] Proper Substitution: df-sb & df-sbc Brian Larson
• 2022/01/03 Re: [Metamath] Updating the website David A. Wheeler
• 2022/01/03 Re: [Metamath] Updating the website Benoit
• 2022/01/03 Re: [Metamath] Pull requests now check for rewrapping Benoit
• 2022/01/03 Re: [Metamath] Re: Metamath distribution Benoit
• 2022/01/02 Re: [Metamath] Pull requests now check for rewrapping Jim Kingdon
• 2022/01/02 Re: [Metamath] Pull requests now check for rewrapping Mario Carneiro
• 2022/01/02 Re: [Metamath] Re: Metamath distribution Mario Carneiro
• 2022/01/02 Re: [Metamath] Updating the website Mario Carneiro
• 2022/01/02 Re: [Metamath] Proper Substitution: df-sb & df-sbc Mario Carneiro
• 2022/01/02 Re: [Metamath] Updating the website David A. Wheeler
• 2022/01/02 [Metamath] Pull requests now check for rewrapping Jim Kingdon
• 2022/01/02 Re: [Metamath] Re: Metamath distribution Benoit
• 2022/01/02 Re: [Metamath] Re: Metamath distribution Jim Kingdon
• 2022/01/02 [Metamath] Re: Metamath distribution Glauco
• 2022/01/02 Re: [Metamath] Updating the website Glauco
• 2022/01/01 Re: [Metamath] Updating the website 'Alexander van der Vekens' via Metamath
• 2022/01/01 Re: [Metamath] Updating the website Glauco
• 2022/01/01 Re: [Metamath] Re: Directed Binary Graph (Lattice) as Irreflexive Poset 'Alexander van der Vekens' via Metamath
• 2021/12/31 Re: [Metamath] Proper Substitution: df-sb & df-sbc Brian Larson
• 2021/12/31 Re: [Metamath] Re: Directed Binary Graph (Lattice) as Irreflexive Poset Brian Larson
• 2021/12/30 [Metamath] Metamath distribution Mario Carneiro
• 2021/12/30 Re: [Metamath] Re: Directed Binary Graph (Lattice) as Irreflexive Poset 'Alexander van der Vekens' via Metamath
• 2021/12/30 Re: [Metamath] Re: Directed Binary Graph (Lattice) as Irreflexive Poset Thierry Arnoux
• 2021/12/30 [Metamath] Re: Directed Binary Graph (Lattice) as Irreflexive Poset 'Alexander van der Vekens' via Metamath
• 2021/12/30 [Metamath] Directed Binary Graph (Lattice) as Irreflexive Poset Brian Larson
• 2021/12/28 Re: [Metamath] Proper Substitution: df-sb & df-sbc Mario Carneiro
• 2021/12/28 Re: [Metamath] Proper Substitution: df-sb & df-sbc David A. Wheeler
• 2021/12/28 Re: [Metamath] Proper Substitution: df-sb & df-sbc Brian Larson
• 2021/12/28 Re: [Metamath] Proper Substitution: df-sb & df-sbc David A. Wheeler
• 2021/12/27 [Metamath] Re: Proper Substitution: df-sb & df-sbc 'Alexander van der Vekens' via Metamath
• 2021/12/27 Re: [Metamath] Proper Substitution: df-sb & df-sbc Thierry Arnoux
• 2021/12/27 [Metamath] Proper Substitution: df-sb & df-sbc Brian Larson
• 2021/12/27 [Metamath] Transitive closure help Scott Fenton
• 2021/12/21 [Metamath] Re: Norman Megill (1950-2021) Jerry James
• 2021/12/20 Re: [Metamath] Discussion: Approving changes to the set.mm database Mario Carneiro
• 2021/12/20 Re: [Metamath] Updating the website Antony Bartlett
• 2021/12/20 Re: [Metamath] Updating the website Antony Bartlett
• 2021/12/20 Re: [Metamath] Discussion: Approving changes to the set.mm database Benoit
• 2021/12/19 Re: [Metamath] Updating the website David A. Wheeler
• 2021/12/19 Re: [Metamath] Updating the website Jim Kingdon
• 2021/12/19 [Metamath] Updating the website Scott Fenton
• 2021/12/19 [Metamath] Re: Proposed change to set.mm repo README 'Alexander van der Vekens' via Metamath
• 2021/12/18 [Metamath] Proposed change to set.mm repo README David A. Wheeler
• 2021/12/16 Re: [Metamath] Norman Megill (1950-2021) Giovanni Mascellani
• 2021/12/15 Re: [Metamath] Discussion: Approving changes to the set.mm database 'Alexander van der Vekens' via Metamath
• 2021/12/14 Re: [Metamath] Discussion: Approving changes to the set.mm database vvs
• 2021/12/14 Re: [Metamath] Discussion: Approving changes to the set.mm database Scott Fenton
• 2021/12/14 Re: [Metamath] Discussion: Approving changes to the set.mm database Scott Fenton
• 2021/12/14 [Metamath] Re: Norman Megill (1950-2021) 'Alexander van der Vekens' via Metamath
• 2021/12/14 Re: [Metamath] Discussion: Approving changes to the set.mm database Jim Kingdon
• 2021/12/14 Re: [Metamath] Discussion: Approving changes to the set.mm database vvs
• 2021/12/14 Re: [Metamath] Discussion: Approving changes to the set.mm database Mario Carneiro
• 2021/12/14 Re: [Metamath] Discussion: Approving changes to the set.mm database vvs
• 2021/12/14 Re: [Metamath] Discussion: Approving changes to the set.mm database David A. Wheeler
• 2021/12/14 Re: [Metamath] Discussion: Approving changes to the set.mm database Mario Carneiro
• 2021/12/14 Re: [Metamath] Discussion: Approving changes to the set.mm database Mario Carneiro
• 2021/12/14 Re: [Metamath] Discussion: Approving changes to the set.mm database David A. Wheeler
• 2021/12/13 [Metamath] Re: Norman Megill (1950-2021) savask
• 2021/12/13 Re: [Metamath] Discussion: Approving changes to the set.mm database Mario Carneiro
• 2021/12/13 Re: [Metamath] Discussion: Approving changes to the set.mm database Mario Carneiro
• 2021/12/13 Re: [Metamath] Discussion: Approving changes to the set.mm database Thierry Arnoux
• 2021/12/13 Re: [Metamath] Completeness Theorem Script Thierry Arnoux
• 2021/12/13 Re: [Metamath] Completeness Theorem Script David A. Wheeler
• 2021/12/13 [Metamath] Completeness Theorem Script Scott Fenton
• 2021/12/13 Re: [Metamath] Discussion: Approving changes to the set.mm database David A. Wheeler
• 2021/12/13 [Metamath] Re: Norman Megill (1950-2021) 'ookami' via Metamath
• 2021/12/13 Re: [Metamath] Re: Discussion: Approving changes to the set.mm database Jim Kingdon
• 2021/12/13 Re: [Metamath] Re: Discussion: Approving changes to the set.mm database Scott Fenton
• 2021/12/13 [Metamath] Re: Discussion: Approving changes to the set.mm database Glauco
• 2021/12/13 [Metamath] Re: Norman Megill (1950-2021) Glauco
• 2021/12/13 Re: [Metamath] Discussion: Approving changes to the set.mm database Jim Kingdon
• 2021/12/13 Re: [Metamath] Discussion: Approving changes to the set.mm database David A. Wheeler
• 2021/12/13 Re: [Metamath] Discussion: Approving changes to the set.mm database Scott Fenton
• 2021/12/13 Re: [Metamath] Norman Megill (1950-2021) Scott Fenton
• 2021/12/13 Re: [Metamath] invalid cert for https://us.metamath.org/ David A. Wheeler
• 2021/12/13 [Metamath] Discussion: Approving changes to the set.mm database David A. Wheeler
• 2021/12/13 Re: [Metamath] Norman Megill (1950-2021) Thierry Arnoux
• 2021/12/13 Re: [Metamath] Norman Megill (1950-2021) Patrick Brosnan
• 2021/12/13 Re: [Metamath] Norman Megill (1950-2021) David A. Wheeler
• 2021/12/13 Re: [Metamath] Re: Norman Megill (1950-2021) Raph Levien
• 2021/12/13 [Metamath] Re: Norman Megill (1950-2021) [email protected]
• 2021/12/13 [Metamath] Re: Norman Megill (1950-2021) vvs
• 2021/12/13 Re: [Metamath] Norman Megill (1950-2021) heiphohmia via Metamath
• 2021/12/13 Re: [Metamath] Norman Megill (1950-2021) Benoit
• 2021/12/12 Re: [Metamath] Norman Megill (1950-2021) Jim Kingdon
• 2021/12/12 Re: [Metamath] Norman Megill (1950-2021) OlivierBinda
• 2021/12/12 Re: [Metamath] Norman Megill (1950-2021) David A. Wheeler
• 2021/12/12 [Metamath] Norman Megill (1950-2021) Mario Carneiro
• 2021/12/11 Re: [Metamath] invalid cert for https://us.metamath.org/ Glauco
• 2021/12/11 Re: [Metamath] invalid cert for https://us.metamath.org/ Ken Kubota
• 2021/12/11 [Metamath] invalid cert for https://us.metamath.org/ Glauco
• 2021/12/10 [Metamath] Re: Two cleanliness scripts Jerry James
• 2021/12/09 Re: [Metamath] StackExchange proposed site ProofAssistants EricGT
• 2021/12/08 Re: [Metamath] Congrats to Scott Fenton on surreal work Scott Fenton
• 2021/12/08 Re: [Metamath] Congrats to Scott Fenton on surreal work Jim Kingdon
• 2021/12/08 [Metamath] Congrats to Scott Fenton on surreal work David A. Wheeler
• 2021/12/07 Re: [Metamath] The set.mm section "Recent label changes" Norman Megill
• 2021/12/06 Re: [Metamath] The set.mm section "Recent label changes" David A. Wheeler
• 2021/12/06 Re: [Metamath] The set.mm section "Recent label changes" 'Alexander van der Vekens' via Metamath
• 2021/12/06 Re: [Metamath] The set.mm section "Recent label changes" 'Alexander van der Vekens' via Metamath
• 2021/12/06 Re: [Metamath] The set.mm section "Recent label changes" Mario Carneiro
• 2021/12/06 Re: [Metamath] The set.mm section "Recent label changes" David A. Wheeler
• 2021/12/05 [Metamath] Re: The set.mm section "Recent label changes" Norman Megill
• 2021/12/05 Re: [Metamath] would fvexd be a bad idea? 'Alexander van der Vekens' via Metamath
• 2021/12/05 Re: [Metamath] Characterization theorems (~ is*) Benoit
• 2021/12/05 [Metamath] The set.mm section "Recent label changes" Benoit
• 2021/12/05 Re: [Metamath] would fvexd be a bad idea? Benoit
• 2021/12/05 Re: [Metamath] would fvexd be a bad idea? 'Alexander van der Vekens' via Metamath
• 2021/12/05 Re: [Metamath] Characterization theorems (~ is*) 'Alexander van der Vekens' via Metamath
• 2021/12/02 Re: [Metamath] Characterization theorems (~ is*) Scott Fenton
• 2021/12/02 [Metamath] Characterization theorems (~ is*) Benoit
• 2021/12/01 Re: [Metamath] Re: Two cleanliness scripts Jerry James
• 2021/12/01 Re: [Metamath] Re: Two cleanliness scripts Glauco
• 2021/12/01 Re: [Metamath] Re: Two cleanliness scripts Norman Megill
• 2021/11/30 Re: [Metamath] Re: Two cleanliness scripts 'Stanislas Polu' via Metamath
• 2021/11/30 Re: [Metamath] Re: Two cleanliness scripts Thierry Arnoux
• 2021/11/30 Re: [Metamath] Suffix d for theorems not in "deduction form" 'Alexander van der Vekens' via Metamath
• 2021/11/30 Re: [Metamath] Re: Two cleanliness scripts 'Alexander van der Vekens' via Metamath
• 2021/11/30 Re: [Metamath] Re: Two cleanliness scripts Jim Kingdon
• 2021/11/30 Re: [Metamath] Re: Two cleanliness scripts Mario Carneiro
• 2021/11/30 [Metamath] Re: Two cleanliness scripts Jerry James
• 2021/11/30 Re: [Metamath] Suffix d for theorems not in "deduction form" Mario Carneiro
• 2021/11/30 Re: [Metamath] Suffix d for theorems not in "deduction form" David A. Wheeler
• 2021/11/30 Re: [Metamath] Re: Erweiterung df-cleq (English translation: Extending df-cleq) Benoit
• 2021/11/30 Re: [Metamath] Suffix d for theorems not in "deduction form" David A. Wheeler
• 2021/11/30 Re: [Metamath] Suffix d for theorems not in "deduction form" David A. Wheeler
• 2021/11/30 Re: [Metamath] Suffix d for theorems not in "deduction form" Benoit
• 2021/11/30 Re: [Metamath] Suffix d for theorems not in "deduction form" Mario Carneiro
• 2021/11/29 Re: [Metamath] Re: Erweiterung df-cleq (English translation: Extending df-cleq) Jim Kingdon
• 2021/11/29 Re: [Metamath] Re: Erweiterung df-cleq (English translation: Extending df-cleq) Norman Megill
• 2021/11/29 Re: [Metamath] Re: Erweiterung df-cleq (English translation: Extending df-cleq) Benoit
• 2021/11/29 Re: [Metamath] Suffix d for theorems not in "deduction form" Benoit
• 2021/11/29 Re: [Metamath] Suffix d for theorems not in "deduction form" David A. Wheeler
• 2021/11/29 Re: [Metamath] Suffix d for theorems not in "deduction form" David A. Wheeler
• 2021/11/29 Re: [Metamath] Suffix d for theorems not in "deduction form" David A. Wheeler
• 2021/11/29 Re: [Metamath] Suffix d for theorems not in "deduction form" Mario Carneiro
• 2021/11/28 Re: [Metamath] Suffix d for theorems not in "deduction form" 'Alexander van der Vekens' via Metamath
• 2021/11/28 Re: [Metamath] Suffix d for theorems not in "deduction form" Norman Megill
• 2021/11/28 Re: [Metamath] Re: Erweiterung df-cleq (English translation: Extending df-cleq) Norman Megill
• 2021/11/28 Re: [Metamath] Suffix d for theorems not in "deduction form" Benoit
• 2021/11/28 Re: [Metamath] Suffix d for theorems not in "deduction form" Jim Kingdon
• 2021/11/28 [Metamath] Re: Suffix d for theorems not in "deduction form" Benoit
• 2021/11/28 [Metamath] Re: Suffix d for theorems not in "deduction form" Benoit
• 2021/11/28 [Metamath] Suffix d for theorems not in "deduction form" 'Alexander van der Vekens' via Metamath
• 2021/11/27 Re: [Metamath] Re: Erweiterung df-cleq (English translation: Extending df-cleq) 'ookami' via Metamath
• 2021/11/27 Re: [Metamath] Re: Erweiterung df-cleq (English translation: Extending df-cleq) Norman Megill
• 2021/11/27 Re: [Metamath] Re: Erweiterung df-cleq (English translation: Extending df-cleq) Benoit
• 2021/11/26 Re: [Metamath] StackExchange proposed site ProofAssistants EricGT
• 2021/11/26 Re: [Metamath] StackExchange proposed site ProofAssistants Mario Carneiro
• 2021/11/25 Re: [Metamath] StackExchange proposed site ProofAssistants Jim Kingdon
• 2021/11/25 [Metamath] StackExchange proposed site ProofAssistants EricGT
• 2021/11/15 Re: [Metamath] Excluding (/) from extensible structure to be a function Mario Carneiro

• Earlier messages
• Later messages