metamath  

Messages by Thread

• • Re: [Metamath] Re: Metamath website 'Alexander van der Vekens' via Metamath
  • Re: [Metamath] Re: Metamath website 'Alexander van der Vekens' via Metamath
• [Metamath] Additional Metamath 100 proof in iset.mm: Bézout's identity Jim Kingdon
  • [Metamath] Re: Additional Metamath 100 proof in iset.mm: Bézout's identity Benoit
  • Re: [Metamath] Re: Additional Metamath 100 proof in iset.mm: Bézout's identity Jim Kingdon
  • Re: [Metamath] Re: Additional Metamath 100 proof in iset.mm: Bézout's identity Benoit
  • Re: [Metamath] Re: Additional Metamath 100 proof in iset.mm: Bézout's identity Jim Kingdon
• [Metamath] Conversation between Stephen Wolfram, Norman Megill and Mario Carneiro savask
  • [Metamath] Re: Conversation between Stephen Wolfram, Norman Megill and Mario Carneiro Benoit
• [Metamath] does "standard" theory assume |- -. +oo e. CC ? Glauco
  • Re: [Metamath] does "standard" theory assume |- -. +oo e. CC ? Jim Kingdon
  • Re: [Metamath] does "standard" theory assume |- -. +oo e. CC ? Glauco
  • Re: [Metamath] does "standard" theory assume |- -. +oo e. CC ? 'Alexander van der Vekens' via Metamath
  • Re: [Metamath] does "standard" theory assume |- -. +oo e. CC ? 'Alexander van der Vekens' via Metamath
  • Re: [Metamath] does "standard" theory assume |- -. +oo e. CC ? Benoit
  • Re: [Metamath] does "standard" theory assume |- -. +oo e. CC ? Thierry Arnoux
  • Re: [Metamath] does "standard" theory assume |- -. +oo e. CC ? Benoit
  • Re: [Metamath] does "standard" theory assume |- -. +oo e. CC ? Glauco
  • Re: [Metamath] does "standard" theory assume |- -. +oo e. CC ? Benoit
  • Re: [Metamath] does "standard" theory assume |- -. +oo e. CC ? Thierry Arnoux
• [Metamath] Pull requests now check for rewrapping Jim Kingdon
  • Re: [Metamath] Pull requests now check for rewrapping Mario Carneiro
  • Re: [Metamath] Pull requests now check for rewrapping Jim Kingdon
  • Re: [Metamath] Pull requests now check for rewrapping Benoit
• [Metamath] Metamath distribution Mario Carneiro
  • [Metamath] Re: Metamath distribution Glauco
  • Re: [Metamath] Re: Metamath distribution Jim Kingdon
  • Re: [Metamath] Re: Metamath distribution Benoit
  • Re: [Metamath] Re: Metamath distribution Mario Carneiro
  • Re: [Metamath] Re: Metamath distribution Benoit
• [Metamath] Directed Binary Graph (Lattice) as Irreflexive Poset Brian Larson
  • [Metamath] Re: Directed Binary Graph (Lattice) as Irreflexive Poset 'Alexander van der Vekens' via Metamath
  • Re: [Metamath] Re: Directed Binary Graph (Lattice) as Irreflexive Poset Thierry Arnoux
  • Re: [Metamath] Re: Directed Binary Graph (Lattice) as Irreflexive Poset 'Alexander van der Vekens' via Metamath
  • Re: [Metamath] Re: Directed Binary Graph (Lattice) as Irreflexive Poset Brian Larson
  • Re: [Metamath] Re: Directed Binary Graph (Lattice) as Irreflexive Poset 'Alexander van der Vekens' via Metamath
• [Metamath] Proper Substitution: df-sb & df-sbc Brian Larson
  • Re: [Metamath] Proper Substitution: df-sb & df-sbc Thierry Arnoux
  • [Metamath] Re: Proper Substitution: df-sb & df-sbc 'Alexander van der Vekens' via Metamath
  • Re: [Metamath] Proper Substitution: df-sb & df-sbc David A. Wheeler
  • Re: [Metamath] Proper Substitution: df-sb & df-sbc Brian Larson
  • Re: [Metamath] Proper Substitution: df-sb & df-sbc David A. Wheeler
  • Re: [Metamath] Proper Substitution: df-sb & df-sbc Mario Carneiro
  • Re: [Metamath] Proper Substitution: df-sb & df-sbc Brian Larson
  • Re: [Metamath] Proper Substitution: df-sb & df-sbc Mario Carneiro
  • Re: [Metamath] Proper Substitution: df-sb & df-sbc Brian Larson
  • Re: [Metamath] Proper Substitution: df-sb & df-sbc Glauco
• [Metamath] Transitive closure help Scott Fenton
• [Metamath] Updating the website Scott Fenton
  • Re: [Metamath] Updating the website Jim Kingdon
  • Re: [Metamath] Updating the website David A. Wheeler
  • Re: [Metamath] Updating the website Antony Bartlett
  • Re: [Metamath] Updating the website Antony Bartlett
  • Re: [Metamath] Updating the website David A. Wheeler
  • Re: [Metamath] Updating the website Mario Carneiro
  • Re: [Metamath] Updating the website Benoit
  • Re: [Metamath] Updating the website David A. Wheeler
  • Re: [Metamath] Updating the website Glauco
  • Re: [Metamath] Updating the website 'Alexander van der Vekens' via Metamath
  • Re: [Metamath] Updating the website Glauco
• [Metamath] Proposed change to set.mm repo README David A. Wheeler
  • [Metamath] Re: Proposed change to set.mm repo README 'Alexander van der Vekens' via Metamath
• [Metamath] Completeness Theorem Script Scott Fenton
  • Re: [Metamath] Completeness Theorem Script David A. Wheeler
  • Re: [Metamath] Completeness Theorem Script Thierry Arnoux
• [Metamath] Discussion: Approving changes to the set.mm database David A. Wheeler
  • Re: [Metamath] Discussion: Approving changes to the set.mm database Scott Fenton
  • Re: [Metamath] Discussion: Approving changes to the set.mm database David A. Wheeler
  • Re: [Metamath] Discussion: Approving changes to the set.mm database Jim Kingdon
  • [Metamath] Re: Discussion: Approving changes to the set.mm database Glauco
  • Re: [Metamath] Re: Discussion: Approving changes to the set.mm database Scott Fenton
  • Re: [Metamath] Re: Discussion: Approving changes to the set.mm database Jim Kingdon
  • Re: [Metamath] Discussion: Approving changes to the set.mm database David A. Wheeler
  • Re: [Metamath] Discussion: Approving changes to the set.mm database Thierry Arnoux
  • Re: [Metamath] Discussion: Approving changes to the set.mm database Mario Carneiro
  • Re: [Metamath] Discussion: Approving changes to the set.mm database Mario Carneiro
  • Re: [Metamath] Discussion: Approving changes to the set.mm database David A. Wheeler
  • Re: [Metamath] Discussion: Approving changes to the set.mm database Mario Carneiro
  • Re: [Metamath] Discussion: Approving changes to the set.mm database Mario Carneiro
  • Re: [Metamath] Discussion: Approving changes to the set.mm database David A. Wheeler
  • Re: [Metamath] Discussion: Approving changes to the set.mm database vvs
  • Re: [Metamath] Discussion: Approving changes to the set.mm database Mario Carneiro
  • Re: [Metamath] Discussion: Approving changes to the set.mm database vvs
  • Re: [Metamath] Discussion: Approving changes to the set.mm database Scott Fenton
  • Re: [Metamath] Discussion: Approving changes to the set.mm database vvs
  • Re: [Metamath] Discussion: Approving changes to the set.mm database 'Alexander van der Vekens' via Metamath
  • Re: [Metamath] Discussion: Approving changes to the set.mm database Benoit
  • Re: [Metamath] Discussion: Approving changes to the set.mm database Mario Carneiro
  • Re: [Metamath] Discussion: Approving changes to the set.mm database Jim Kingdon
  • Re: [Metamath] Discussion: Approving changes to the set.mm database Scott Fenton
• [Metamath] Norman Megill (1950-2021) Mario Carneiro
  • Re: [Metamath] Norman Megill (1950-2021) David A. Wheeler
  • Re: [Metamath] Norman Megill (1950-2021) OlivierBinda
  • Re: [Metamath] Norman Megill (1950-2021) Jim Kingdon
  • Re: [Metamath] Norman Megill (1950-2021) Benoit
  • Re: [Metamath] Norman Megill (1950-2021) heiphohmia via Metamath
  • [Metamath] Re: Norman Megill (1950-2021) vvs
  • [Metamath] Re: Norman Megill (1950-2021) [email protected]
  • Re: [Metamath] Re: Norman Megill (1950-2021) Raph Levien
  • Re: [Metamath] Norman Megill (1950-2021) David A. Wheeler
  • Re: [Metamath] Norman Megill (1950-2021) Patrick Brosnan
  • Re: [Metamath] Norman Megill (1950-2021) Thierry Arnoux
  • Re: [Metamath] Norman Megill (1950-2021) Scott Fenton
  • [Metamath] Re: Norman Megill (1950-2021) Glauco
  • [Metamath] Re: Norman Megill (1950-2021) 'ookami' via Metamath
  • [Metamath] Re: Norman Megill (1950-2021) savask
  • [Metamath] Re: Norman Megill (1950-2021) 'Alexander van der Vekens' via Metamath
  • Re: [Metamath] Norman Megill (1950-2021) Giovanni Mascellani
  • [Metamath] Re: Norman Megill (1950-2021) Jerry James
• [Metamath] invalid cert for https://us.metamath.org/ Glauco
  • Re: [Metamath] invalid cert for https://us.metamath.org/ Ken Kubota
  • Re: [Metamath] invalid cert for https://us.metamath.org/ Glauco
  • Re: [Metamath] invalid cert for https://us.metamath.org/ David A. Wheeler
• [Metamath] Congrats to Scott Fenton on surreal work David A. Wheeler
  • Re: [Metamath] Congrats to Scott Fenton on surreal work Jim Kingdon
  • Re: [Metamath] Congrats to Scott Fenton on surreal work Scott Fenton
• [Metamath] The set.mm section "Recent label changes" Benoit
  • [Metamath] Re: The set.mm section "Recent label changes" Norman Megill
  • Re: [Metamath] The set.mm section "Recent label changes" David A. Wheeler
  • Re: [Metamath] The set.mm section "Recent label changes" Mario Carneiro
  • Re: [Metamath] The set.mm section "Recent label changes" 'Alexander van der Vekens' via Metamath
  • Re: [Metamath] The set.mm section "Recent label changes" 'Alexander van der Vekens' via Metamath
  • Re: [Metamath] The set.mm section "Recent label changes" David A. Wheeler
  • Re: [Metamath] The set.mm section "Recent label changes" Norman Megill
• [Metamath] Characterization theorems (~ is*) Benoit
  • Re: [Metamath] Characterization theorems (~ is*) Scott Fenton
  • Re: [Metamath] Characterization theorems (~ is*) 'Alexander van der Vekens' via Metamath
  • Re: [Metamath] Characterization theorems (~ is*) Benoit
• [Metamath] Suffix d for theorems not in "deduction form" 'Alexander van der Vekens' via Metamath
  • [Metamath] Re: Suffix d for theorems not in "deduction form" Benoit
  • [Metamath] Re: Suffix d for theorems not in "deduction form" Benoit
  • Re: [Metamath] Suffix d for theorems not in "deduction form" Jim Kingdon
  • Re: [Metamath] Suffix d for theorems not in "deduction form" Benoit
  • Re: [Metamath] Suffix d for theorems not in "deduction form" Norman Megill
  • Re: [Metamath] Suffix d for theorems not in "deduction form" 'Alexander van der Vekens' via Metamath
  • Re: [Metamath] Suffix d for theorems not in "deduction form" Mario Carneiro
  • Re: [Metamath] Suffix d for theorems not in "deduction form" David A. Wheeler
  • Re: [Metamath] Suffix d for theorems not in "deduction form" David A. Wheeler
  • Re: [Metamath] Suffix d for theorems not in "deduction form" David A. Wheeler
  • Re: [Metamath] Suffix d for theorems not in "deduction form" Benoit
  • Re: [Metamath] Suffix d for theorems not in "deduction form" Mario Carneiro
  • Re: [Metamath] Suffix d for theorems not in "deduction form" Benoit
  • Re: [Metamath] Suffix d for theorems not in "deduction form" David A. Wheeler
  • Re: [Metamath] Suffix d for theorems not in "deduction form" David A. Wheeler
  • Re: [Metamath] Suffix d for theorems not in "deduction form" Mario Carneiro
  • Re: [Metamath] Suffix d for theorems not in "deduction form" 'Alexander van der Vekens' via Metamath
  • Re: [Metamath] Suffix d for theorems not in "deduction form" David A. Wheeler
• [Metamath] StackExchange proposed site ProofAssistants EricGT
  • Re: [Metamath] StackExchange proposed site ProofAssistants Jim Kingdon
  • Re: [Metamath] StackExchange proposed site ProofAssistants Mario Carneiro
  • Re: [Metamath] StackExchange proposed site ProofAssistants EricGT
  • Re: [Metamath] StackExchange proposed site ProofAssistants EricGT
  • Re: [Metamath] StackExchange proposed site ProofAssistants EricGT
• [Metamath] Excluding (/) from extensible structure to be a function 'Alexander van der Vekens' via Metamath
  • Re: [Metamath] Excluding (/) from extensible structure to be a function Mario Carneiro
  • Re: [Metamath] Excluding (/) from extensible structure to be a function 'Alexander van der Vekens' via Metamath
  • Re: [Metamath] Excluding (/) from extensible structure to be a function David A. Wheeler
  • Re: [Metamath] Excluding (/) from extensible structure to be a function Mario Carneiro
• [Metamath] AGI research on metamath and grant proposals Jon P
• [Metamath] Valuation Jim Kingdon
  • Re: [Metamath] Valuation Thierry Arnoux
  • Re: [Metamath] Valuation Kyle Wyonch
  • Re: [Metamath] Valuation Jim Kingdon
• [Metamath] Mandatory "standard" formatting prior to submitting a pull request? Glauco
  • Re: [Metamath] Mandatory "standard" formatting prior to submitting a pull request? Mario Carneiro
  • Re: [Metamath] Mandatory "standard" formatting prior to submitting a pull request? Jim Kingdon
  • Re: [Metamath] Mandatory "standard" formatting prior to submitting a pull request? Glauco
  • [Metamath] Re: Mandatory "standard" formatting prior to submitting a pull request? 'Alexander van der Vekens' via Metamath
  • [Metamath] Re: Mandatory "standard" formatting prior to submitting a pull request? Benoit
  • [Metamath] Re: Mandatory "standard" formatting prior to submitting a pull request? Norman Megill
• [Metamath] Superior limit Benoit
• [Metamath] Meta 'Alexander van der Vekens' via Metamath
  • [Metamath] Re: Meta Benoit
• [Metamath] Two cleanliness scripts Jerry James
  • Re: [Metamath] Two cleanliness scripts Thierry Arnoux
  • Re: [Metamath] Two cleanliness scripts Benoit
  • Re: [Metamath] Two cleanliness scripts Jerry James
  • Re: [Metamath] Two cleanliness scripts Benoit
  • Re: [Metamath] Two cleanliness scripts Jerry James
  • Re: [Metamath] Two cleanliness scripts Benoit
  • Re: [Metamath] Two cleanliness scripts Jerry James
  • Re: [Metamath] Two cleanliness scripts Benoit
  • Re: [Metamath] Two cleanliness scripts Jerry James
  • Re: [Metamath] Two cleanliness scripts Benoit
  • Re: [Metamath] Two cleanliness scripts Jerry James
  • Re: [Metamath] Two cleanliness scripts Jerry James
  • [Metamath] Re: Two cleanliness scripts Jerry James
  • Re: [Metamath] Re: Two cleanliness scripts Mario Carneiro
  • Re: [Metamath] Re: Two cleanliness scripts Glauco
  • Re: [Metamath] Re: Two cleanliness scripts Jim Kingdon
  • Re: [Metamath] Re: Two cleanliness scripts 'Alexander van der Vekens' via Metamath
  • Re: [Metamath] Re: Two cleanliness scripts Thierry Arnoux
  • Re: [Metamath] Re: Two cleanliness scripts 'Stanislas Polu' via Metamath
  • Re: [Metamath] Re: Two cleanliness scripts Norman Megill
  • Re: [Metamath] Re: Two cleanliness scripts Jerry James
  • [Metamath] Re: Two cleanliness scripts Jerry James
• [Metamath] Definitions vs "conservative and eliminable" Cris Perdue
• [Metamath] Erweiterung df-cleq 'ookami' via Metamath
  • [Metamath] Re: Erweiterung df-cleq Norman Megill
  • [Metamath] Re: Erweiterung df-cleq (English translation: Extending df-cleq) 'ookami' via Metamath

• Earlier messages
• Later messages