issues
search
metamath
/
set.mm
Metamath source file for logic and set theory
Creative Commons Zero v1.0 Universal
237
stars
86
forks
source link
issues
Newest
Newest
Most commented
Recently updated
Oldest
Least commented
Least recently updated
ax-strcoll and ax-sscoll in iset.mm are inconsistent
#4077
CatsAreFluffy
opened
6 hours ago
0
prove qnnen via Stern’s diatomic sequence
#4076
jkingdon
opened
1 day ago
1
Start of construction of solution
#4075
metakunt
opened
1 day ago
1
Rename syl6eq to eqtrdi
#4074
jkingdon
closed
1 day ago
3
Replace syl6reqr with eqtr4id
#4073
jkingdon
closed
2 days ago
1
Revise ficardun and related theorems
#4072
BTernaryTau
closed
3 days ago
1
A pass through section "Existence of omega (the set of natural numbers)"
#4071
jkingdon
closed
4 days ago
0
The Zariski Topology is compact
#4070
tirix
closed
3 days ago
2
Strengthen sbthom from LPO→EXMID to MP→EXMID
#4069
jkingdon
opened
1 week ago
0
0a = 0 (mulcom pr 10)
#4068
icecream17
closed
4 days ago
1
Decidable equality for real numbers (analytic WLPO) implies equinumerosity of open and closed intervals
#4067
jkingdon
opened
1 week ago
0
iset.mm: two theorems related to equinumerosity of real numbers
#4066
jkingdon
closed
1 week ago
0
Reduce axiom usage
#4065
GinoGiotto
closed
1 week ago
0
Rename syl6req to eqtr2di
#4064
jkingdon
closed
1 week ago
0
Several utility theorems
#4063
tirix
closed
1 week ago
1
If not equal implies apart, Markov's principle follows
#4062
jkingdon
closed
1 week ago
0
ax-mulcom pr 9 (mulgt0 results)
#4061
icecream17
closed
1 week ago
1
Add dcapncf to iset.mm
#4060
jkingdon
closed
1 week ago
0
wl-df3maxtru1
#4059
wlammen
closed
2 weeks ago
0
Lesser limited principle of omniscience
#4058
jkingdon
opened
2 weeks ago
0
Decidability of real number equality implies WLPO
#4057
jkingdon
closed
2 weeks ago
0
finish intuitionizing "The natural logarithm on complex numbers" section
#4056
jkingdon
closed
2 weeks ago
0
wl-df4-3mintru2
#4055
wlammen
closed
2 weeks ago
0
fix missing date/typo
#4054
wlammen
closed
2 weeks ago
0
mathbox wl-ifp4impr
#4053
wlammen
closed
2 weeks ago
0
Two NN+oo equivalences
#4052
jkingdon
opened
2 weeks ago
0
Polynomial matrices form an associative algebra
#4051
avekens
closed
2 weeks ago
0
fsuppssind
#4050
icecream17
closed
1 week ago
3
The Zariski topology is a topology
#4049
tirix
closed
2 weeks ago
2
Rename syl6eqr to eqtr4di
#4048
jkingdon
closed
3 weeks ago
5
intuitionize ^c from df-cxp to cxplea
#4047
jkingdon
closed
3 weeks ago
0
move section "Associative algebras"
#4046
icecream17
closed
3 weeks ago
0
disjunctive normal form for wl-df-3mintru2
#4045
wlammen
closed
3 weeks ago
0
First pass at intuitionizing the rest of the "The natural logarithm on complex numbers" section
#4044
jkingdon
closed
3 weeks ago
0
Add trirec0 to iset.mm
#4043
jkingdon
closed
3 weeks ago
0
Equinumerosity of open and closed intervals implies WLPO
#4042
jkingdon
opened
4 weeks ago
0
decidability of real number equality implies WLPO
#4041
jkingdon
closed
2 weeks ago
0
Add WLPO to iset.mm
#4040
jkingdon
closed
3 weeks ago
1
expand mmil.html from dvmptim to dvexp3
#4039
jkingdon
closed
4 weeks ago
0
Theorem 6.6 Aks Inequality
#4038
metakunt
closed
3 weeks ago
3
rename NaryF to -aryF and switch args
#4037
icecream17
closed
4 weeks ago
1
Add iccioo01 to set.mm mathbox.
#4036
jkingdon
closed
1 month ago
1
rename symbol NaryF to -aryF
#4035
icecream17
closed
4 weeks ago
0
n-ary functions (2)
#4034
avekens
closed
1 month ago
10
use spvv in nfcr, paragraph html fix
#4033
icecream17
closed
1 month ago
2
Prove ~rabeqi without ax-12
#4032
GinoGiotto
closed
1 month ago
0
iset.mm: fix metamath-knife build error and a few derivative notes/theorems
#4031
jkingdon
closed
1 month ago
1
Semiring of ideals (1)
#4030
tirix
closed
1 month ago
0
ax-mulcom pr 8, more structure deductions
#4029
icecream17
closed
1 month ago
0
add immediate version of fndm and shorten proofs with it
#4028
wlammen
closed
1 month ago
1
Next