Formalized theorems

entries per page

Search:

MSC	Name	Isabelle	HOL Light	Rocq	Lean	Metamath	Mizar
26	Abel's theorem				L
12	Abel–Ruffini theorem				L
68	Akra–Bazzi theorem				L
11	Apéry's theorem				X
91	Arrow's impossibility theorem				X
16	Artin–Wedderburn theorem				L
46	Arzelà–Ascoli theorem				L
03	Ax–Grothendieck theorem				L
54	Baire category theorem				L
54	Banach fixed-point theorem				L
46	Banach–Alaoglu theorem				L
46	Banach–Steinhaus theorem				L
26	Basel problem				L
60	Bayes' theorem				L
18	Beck's monadicity theorem				L
60	Bertrand's ballot theorem				L
11	Bertrand's postulate				L
26	Besicovitch covering theorem				L
05	Binomial theorem				L
06	Birkhoff's representation theorem				L
15	Birkhoff–Von Neumann theorem				L
26	Bolzano–Weierstrass theorem				L
28	Bounded convergence theorem				L
54	Brouwer fixed-point theorem				X
26	Cantor's intersection theorem				L
03	Cantor's theorem				L
03	Cantor–Bernstein–Schroeder theorem	S	S	X	L	L	L
52	Carathéodory's theorem				L
28	Carathéodory's theorem				L
30	Cauchy integral theorem				L
20	Cauchy's theorem				L
20	Cayley's theorem				L
15	Cayley–Hamilton theorem				L
12	Chevalley–Warning theorem				L
11	Chinese remainder theorem				L
46	Closed graph theorem				L
03	Compactness theorem				L
11	Corners theorem				L
30	De Moivre's theorem				L
15	Dimension theorem for vector spaces				L
26	Dini's theorem				L
11	Dirichlet's theorem on arithmetic progressions				L
28	Dominated convergence theorem				L
28	Egorov's theorem				L
11	Erdős–Ginzburg–Ziv theorem				L
05	Erdős–Ko–Rado theorem				L
52	Erdős–Szekeres theorem				L
11	Euclid's theorem				L
11	Euclid–Euler theorem				L
11	Euler's partition theorem				L
26	Extreme value theorem				L
26	Fatou–Lebesgue theorem				L
11	Fermat's Last Theorem				L
11	Fermat's little theorem				L
11	Fermat's theorem on sums of two squares				L
05	Four functions theorem				L
43	Fourier inversion theorem				L
05	Friendship theorem				L
28	Fubini's theorem				L
30	Fundamental theorem of algebra				L
11	Fundamental theorem of arithmetic				L
26	Fundamental theorem of calculus				L
16	Fundamental theorem on homomorphisms				L
03	Gödel's incompleteness theorem				X
30	Hadamard three-lines theorem				L
28	Hahn decomposition theorem				L
46	Hahn–Banach theorem				L
05	Hales–Jewett theorem				L
05	Hall's marriage theorem				L
30	Hartogs's theorem				X
26	Heine–Borel theorem				L
51	Heine–Cantor theorem				L
52	Helly's theorem				L
46	Hilbert projection theorem				L
13	Hilbert's basis theorem				L
14	Hilbert's Nullstellensatz (theorem of zeroes)				L
05	Hindman's theorem				L
30	Identity theorem				L
26	Implicit function theorem				L
03	Independence of the continuum hypothesis				X
12	Integral root theorem				L
26	Intermediate value theorem				L
26	Inverse function theorem				L
16	Isomorphism theorem				L
20	Jordan–Hölder theorem				L
06	Kleene fixed-point theorem				L
03	Kleene's recursion theorem				L
06	Knaster–Tarski theorem				L
05	Kneser's theorem				X
60	Kolmogorov extension theorem				X
52	Krein–Milman theorem				L
05	Kruskal–Katona theorem				L
11	Lagrange's four-square theorem				L
20	Lagrange's theorem				L
13	Lasker–Noether theorem				L
16	Lattice theorem				L
35	Lax–Milgram theorem				L
26	Lebesgue differentiation theorem				L
54	Lebesgue's decomposition theorem				L
54	Lebesgue's density theorem				L

Showing 1 to 100 of 165 entries