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

99 Open 271 Closed
99 Open 271 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

Move ODual to the top of Part 9?
#4253 opened Sep 27, 2024 by zwang123
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
5
Definition of the greatest common divisor enhancement
#4161 opened Aug 24, 2024 by benjub
3
df-cdeq
#4158 opened Aug 23, 2024 by icecream17
1
1
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
9
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
Equinumerosity of open and closed intervals implies WLPO
#4042 opened Jun 10, 2024 by jkingdon
Feedback from a new user, improvement suggestions.
#3990 opened May 16, 2024 by metakunt
23
Can a space filling curve exist in iset.mm?
#3812 opened Feb 1, 2024 by jkingdon
5
Update of the topological structure overview figure
#3805 opened Jan 29, 2024 by tirix
4
Updating mmset.html
#3762 opened Jan 13, 2024 by wlammen
12
ProTip! Follow long discussions with comments:>50.