Wikipedia’s list of theorems

Content created by Fredrik Bakke and Louis Wasserman.

Created on 2025-08-30.
Last modified on 2026-02-20.

On this page, we record formalized results in the agda-unimath library that are on Wikipedia’s list of theorems or have a Wikidata entry listed as an instance of a theorem. Additions to this list are very welcome!

module literature.wikipedia-list-of-theorems where

Formalized theorems

The theorems are ordered alphabetically, omitting leading definite articles (“the”).

Absolute convergence theorem

Author: Louis Wasserman

open import analysis.absolute-convergence-series-real-numbers using
  ( is-convergent-is-absolutely-convergent-series-ℝ)
open import functional-analysis.absolute-convergence-series-real-banach-spaces using
  ( is-convergent-is-absolutely-convergent-series-ℝ-Banach-Space)

Bézout’s lemma

Author: Bryan Lu

open import elementary-number-theory.bezouts-lemma-integers using
  ( bezouts-lemma-ℤ)
open import elementary-number-theory.bezouts-lemma-natural-numbers using
  ( bezouts-lemma-ℕ)

Binomial theorem

Author: Egbert Rijke

open import commutative-algebra.binomial-theorem-commutative-rings using
  ( binomial-theorem-Commutative-Ring)
open import commutative-algebra.binomial-theorem-commutative-semirings using
  ( binomial-theorem-Commutative-Semiring)
open import ring-theory.binomial-theorem-rings using
  ( binomial-theorem-Ring)
open import ring-theory.binomial-theorem-semirings using
  ( binomial-theorem-Semiring)
open import elementary-number-theory.binomial-theorem-integers using
  ( binomial-theorem-ℤ)
open import elementary-number-theory.binomial-theorem-natural-numbers using
  ( binomial-theorem-ℕ)

Cantor–Schröder–Bernstein theorem

Author: Elif Uskuplu

open import foundation.cantor-schroder-bernstein-escardo using
  ( Cantor-Schröder-Bernstein-Escardó ;
    Cantor-Schröder-Bernstein)

Author: Fredrik Bakke

open import foundation.cantor-schroder-bernstein-decidable-embeddings using
  ( Cantor-Schröder-Bernstein-WLPO)

Cantor’s theorem

Author: Egbert Rijke

open import foundation.cantors-theorem using
  ( theorem-Cantor)

Cayley’s theorem

Author: Egbert Rijke

open import group-theory.cayleys-theorem using
  ( Cayleys-theorem)

Cauchy-Schwarz inequality

Author: Louis Wasserman and malarbol

open import linear-algebra.cauchy-schwarz-inequality-real-inner-product-spaces using
  ( cauchy-schwarz-inequality-ℝ-Inner-Product-Space)

Diaconescu’s theorem

Author: Fredrik Bakke

open import foundation.diaconescus-theorem using
  ( theorem-Diaconescu)

Euclid’s theorem

Author: Egbert Rijke

open import elementary-number-theory.infinitude-of-primes using
  ( infinitude-of-primes-ℕ)

Fundamental theorem of arithmetic

Author: Victor Blanchi

open import elementary-number-theory.fundamental-theorem-of-arithmetic using
  ( fundamental-theorem-arithmetic-list-ℕ)

Fundamental theorem of equivalence relations

Author: Egbert Rijke

open import foundation.fundamental-theorem-of-equivalence-relations using
  ( equiv-equivalence-relation-partition)

Fundamental theorem on homomorphisms

Author: Egbert Rijke

open import group-theory.quotient-groups using
  ( is-quotient-group-quotient-Group)

Intermediate Value Theorem

Author: Louis Wasserman

open import analysis.intermediate-value-theorem using
  ( intermediate-value-theorem-ℝ)
open import analysis.constructive-intermediate-value-theorem using
  ( constructive-intermediate-value-theorem-ℝ)

Kleene’s fixed point theorem

Author: Fredrik Bakke

open import domain-theory.kleenes-fixed-point-theorem-posets using
  ( is-least-fixed-point-theorem-kleene-hom-Poset ;
    is-least-fixed-point-theorem-kleene-Poset)
open import domain-theory.kleenes-fixed-point-theorem-omega-complete-posets using
  ( is-least-fixed-point-theorem-kleene-hom-ω-Complete-Poset ;
    is-least-fixed-point-theorem-kleene-ω-Complete-Poset)

Knaster–Tarski fixed point theorem

Author: Fredrik Bakke

open import order-theory.knaster-tarski-fixed-point-theorem using
  ( least-fixed-point-knaster-tarski-Inflattice ;
    greatest-fixed-point-knaster-tarski-Suplattice)

Lawvere’s fixed point theorem

Author: Egbert Rijke

open import foundation.lawveres-fixed-point-theorem using
  ( fixed-point-theorem-Lawvere)

Monotone convergence theorem

Author: Fredrik Bakke

open import analysis.monotone-convergence-theorem-increasing-sequences-real-numbers using
  ( is-limit-is-modulated-supremum-is-increasing-sequence-ℝ ;
    is-limit-is-supremum-is-increasing-sequence-ACℕ-ℝ)

Pythagorean theorem

Author: Louis Wasserman

open import linear-algebra.orthogonality-real-inner-product-spaces using
  ( pythagorean-theorem-ℝ-Inner-Product-Space)

Squeeze theorem

Author: Louis Wasserman

open import real-numbers.cauchy-sequences-real-numbers using
  ( is-cauchy-squeeze-theorem-sequence-ℝ)

Triangle inequality theorem

Author: malarbol

open import real-numbers.metric-space-of-real-numbers using
  ( is-triangular-neighborhood-ℝ)

Author: Louis Wasserman

open import real-numbers.absolute-value-real-numbers using
  ( triangle-inequality-abs-ℝ)
open import real-numbers.distance-real-numbers using
  ( triangle-inequality-dist-ℝ)

Uniform limit theorem

Author: Fredrik Bakke

open import metric-spaces.uniform-limit-theorem-pointwise-continuous-maps-metric-spaces using
  ( is-pointwise-ε-δ-continuous-map-is-uniform-limit-sequence-map-Metric-Space ;
    is-pointwise-continuous-map-is-uniform-limit-sequence-map-ACℕ-Metric-Space)
open import metric-spaces.uniform-limit-theorem-uniformly-continuous-maps-metric-spaces using
  ( modulus-of-uniform-continuity-map-limit-modulus-sequence-map-Metric-Space ;
    is-uniformly-continuous-map-is-uniform-limit-sequence-map-Metric-Space ;
    is-uniformly-continuous-map-is-uniform-limit-sequence-map-ACℕ-Metric-Space)

Yoneda lemma

Author: Emily Riehl

open import category-theory.yoneda-lemma-categories using
  ( lemma-yoneda-Category)
open import category-theory.yoneda-lemma-precategories using
  ( lemma-yoneda-Precategory)

Recent changes