Skip to content

Issues: metamath/set.mm

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

103 Open 277 Closed
103 Open 277 Closed
Author
Filter by author
Loading
Label
Filter by label
Loading
Use alt + click/return to exclude labels
or ⇧ + click/return for logical OR
Projects
Filter by project
Loading
Milestones
Filter by milestone
Loading
Assignee
Filter by who’s assigned
Sort
Sort by
Newest Oldest Most commented Least commented Recently updated Least recently updated Best match
Most reactions
👍 👎 😄 🎉 😕 ❤️ 🚀 👀

Issues list

decidability theorems in iset.mm could be a bit better structured
#4384 opened Nov 11, 2024 by jkingdon
7
Definition for LatRel and reactivation of the related theorems
#4302 opened Oct 20, 2024 by avekens
If not rational implies irrational, then <some constructive taboo>
#4299 opened Oct 17, 2024 by jkingdon
7
Enable github discussions for this project (or metamath organization)
#4288 opened Oct 13, 2024 by savask
10
Total ordering needed for recursion ?
#4279 opened Oct 12, 2024 by benjub
9
Remove ax-riotaBAD [mathbox]
#4265 opened Oct 4, 2024 by icecream17
Move ODual to the top of Part 9?
#4253 opened Sep 27, 2024 by zwang123
5
The Impossibility of Trisecting the Angle and Doubling the Cube (metamath 100 #8) metamath 100
#4246 opened Sep 25, 2024 by tirix
2
Use a merge queue to check for verification failures before merging pull requests
#4228 opened Sep 22, 2024 by BTernaryTau
9
Definition of the Euler--Mascheroni constant
#4227 opened Sep 21, 2024 by benjub
Would using Tectonic speed up the set.mm TeX build?
#4196 opened Sep 9, 2024 by jkingdon
Cantor Normal Form in set.mm
#4171 opened Aug 29, 2024 by sctfn
6
Definition of the greatest common divisor enhancement
#4161 opened Aug 24, 2024 by benjub
3
The type ℕ∞ has decidable equality iff WLPO holds
#4151 opened Aug 22, 2024 by jkingdon
1
Extensible structures whose components are proper classes?
#4145 opened Aug 20, 2024 by zwang123
15
Terminal objects are initial objects in the opposite category
#4142 opened Aug 19, 2024 by zwang123
6
Definition of the structure product (df-prds)
#4135 opened Aug 16, 2024 by zwang123
9
Definition of complex number apartness looks too strong
#4131 opened Aug 15, 2024 by benjub
1
change degree of zero polynomial for df-dgr from 0 to -inf
#4102 opened Jul 28, 2024 by icecream17
3
A continuity principle involving NN+oo
#4087 opened Jul 19, 2024 by jkingdon
prove qnnen via Stern’s diatomic sequence
#4076 opened Jul 7, 2024 by jkingdon
1
Strengthen sbthom from LPO→EXMID to MP→EXMID
#4069 opened Jul 1, 2024 by jkingdon
Decidable equality for real numbers (analytic WLPO) implies equinumerosity of open and closed intervals
#4067 opened Jun 30, 2024 by jkingdon
Lesser limited principle of omniscience
#4058 opened Jun 22, 2024 by jkingdon
Two NN+oo equivalences
#4052 opened Jun 17, 2024 by jkingdon
ProTip! Follow long discussions with comments:>50.