1000+ theorems

Freek Wiedijk started the 1000+ theorems project tracking progress of theorem provers in formalizing named theorems on wikipedia, as a way of comparing prominent theorem provers. Currently 157 of them are formalized in Lean, and 2 additional theorem(s) have just their statement formalized in Lean. We also have a page with the theorems from the list not yet in Lean.

To make updates to this list, please make a pull request to mathlib after editing the yaml source file. This can be done entirely on GitHub, see "Editing files in another user's repository".

Q11518: Pythagorean theorem #

Author: Joseph Myers

theorem EuclideanGeometry.dist_sq_eq_dist_sq_add_dist_sq_iff_angle_eq_pi_div_two {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] (p1 p2 p3 : P) :
dist p1 p3 * dist p1 p3 = dist p1 p2 * dist p1 p2 + dist p3 p2 * dist p3 p2 ↔ EuclideanGeometry.angle p1 p2 p3 = Real.pi / 2

docs, source

Q26708: Binomial theorem #

Author: Chris Hughes

theorem add_pow {R : Type u_1} [CommSemiring R] (x y : R) (n : ℕ) :
(x + y) ^ n = ∑ m ∈ Finset.range (n + 1), x ^ m * y ^ (n - m) * ↑(n.choose m)

docs, source

Q33481: Arrow's impossibility theorem #

Author: Benjamin Davidson, Andrew Souther

url

Q137164: Besicovitch covering theorem #

Author: Sébastien Gouëzel

theorem Besicovitch.exists_disjoint_closedBall_covering_ae {α : Type u_1} [MetricSpace α] [SecondCountableTopology α] [MeasurableSpace α] [OpensMeasurableSpace α] [HasBesicovitchCovering α] (μ : MeasureTheory.Measure α) [MeasureTheory.SFinite μ] (f : α → Set ℝ) (s : Set α) (hf : ∀ x ∈ s, ∀ δ > 0, (f x ∩ Set.Ioo 0 δ).Nonempty) (R : α → ℝ) (hR : ∀ x ∈ s, 0 < R x) :
∃ (t : Set α) (r : α → ℝ), t.Countable ∧ t ⊆ s ∧ (∀ x ∈ t, r x ∈ f x ∩ Set.Ioo 0 (R x)) ∧ μ (s \ ⋃ x ∈ t, Metric.closedBall x (r x)) = 0 ∧ t.PairwiseDisjoint fun (x : α) => Metric.closedBall x (r x)

docs, source

Q172298: Lasker–Noether theorem #
theorem Ideal.isPrimary_decomposition_pairwise_ne_radical {R : Type u_1} [CommSemiring R] {I : Ideal R} {s : Finset (Ideal R)} (hs : s.inf id = I) (hs' : ∀ ⦃J : Ideal R⦄, J ∈ s → J.IsPrimary) :
∃ (t : Finset (Ideal R)), t.inf id = I ∧ (∀ ⦃J : Ideal R⦄, J ∈ t → J.IsPrimary) ∧ (↑t).Pairwise (Function.onFun (fun (x1 x2 : Ideal R) => x1 ≠ x2) Ideal.radical)

docs, source

Q179208: Cayley's theorem #

Author: Eric Wieser

noncomputable def Equiv.Perm.subgroupOfMulAction (G : Type u_1) (H : Type u_2) [Group G] [MulAction G H] [FaithfulSMul G H] :
G ≃* ↥(MulAction.toPermHom G H).range

docs, source

Q180345X: Integral root theorem #
theorem isInteger_of_is_root_of_monic {A : Type u_1} {K : Type u_2} [CommRing A] [IsDomain A] [UniqueFactorizationMonoid A] [Field K] [Algebra A K] [IsFractionRing A K] {p : Polynomial A} (hp : p.Monic) {r : K} (hr : (Polynomial.aeval r) p = 0) :
IsLocalization.IsInteger A r

docs, source

Q180345: Rational root theorem #
theorem num_dvd_of_is_root {A : Type u_1} {K : Type u_2} [CommRing A] [IsDomain A] [UniqueFactorizationMonoid A] [Field K] [Algebra A K] [IsFractionRing A K] {p : Polynomial A} {r : K} (hr : (Polynomial.aeval r) p = 0) :
IsFractionRing.num A r ∣ p.coeff 0

docs, source

theorem den_dvd_of_is_root {A : Type u_1} {K : Type u_2} [CommRing A] [IsDomain A] [UniqueFactorizationMonoid A] [Field K] [Algebra A K] [IsFractionRing A K] {p : Polynomial A} {r : K} (hr : (Polynomial.aeval r) p = 0) :
↑(IsFractionRing.den A r) ∣ p.leadingCoeff

docs, source

Q182505: Bayes' theorem #

Author: Rishikesh Vaishnav

theorem ProbabilityTheory.cond_eq_inv_mul_cond_mul {Ω : Type u_1} {m : MeasurableSpace Ω} {s t : Set Ω} (hms : MeasurableSet s) (hmt : MeasurableSet t) (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsFiniteMeasure μ] :
(ProbabilityTheory.cond μ s) t = (μ s)⁻¹ * (ProbabilityTheory.cond μ t) s * μ t

docs, source

Q188295: Fermat's little theorem #

Author: Aaron Anderson

theorem ZMod.pow_card_sub_one_eq_one {p : ℕ} [Fact (Nat.Prime p)] {a : ZMod p} (ha : a ≠ 0) :
a ^ (p - 1) = 1

docs, source

Q189136: Mean value theorem #

Author: Yury G. Kudryashov

theorem exists_deriv_eq_slope (f : ℝ → ℝ) {a b : ℝ} (hab : a < b) (hfc : ContinuousOn f (Set.Icc a b)) (hfd : DifferentiableOn ℝ f (Set.Ioo a b)) :
∃ c ∈ Set.Ioo a b, deriv f c = (f b - f a) / (b - a)

docs, source

theorem exists_ratio_deriv_eq_ratio_slope (f : ℝ → ℝ) {a b : ℝ} (hab : a < b) (hfc : ContinuousOn f (Set.Icc a b)) (hfd : DifferentiableOn ℝ f (Set.Ioo a b)) (g : ℝ → ℝ) (hgc : ContinuousOn g (Set.Icc a b)) (hgd : DifferentiableOn ℝ g (Set.Ioo a b)) :
∃ c ∈ Set.Ioo a b, (g b - g a) * deriv f c = (f b - f a) * deriv g c

docs, source

Q190556: De Moivre's theorem #

Author: Abhimanyu Pallavi Sudhir

theorem Complex.cos_add_sin_mul_I_pow (n : ℕ) (z : ℂ) :
(Complex.cos z + Complex.sin z * Complex.I) ^ n = Complex.cos (↑n * z) + Complex.sin (↑n * z) * Complex.I

docs, source

Q191693: Lebesgue's decomposition theorem #

Author: Kexing Ying

instance MeasureTheory.Measure.haveLebesgueDecomposition_of_sigmaFinite {α : Type u_1} {m : MeasurableSpace α} (μ ν : MeasureTheory.Measure α) [MeasureTheory.SFinite μ] [MeasureTheory.SigmaFinite ν] :
μ.HaveLebesgueDecomposition ν

docs, source

Q192760: Fundamental theorem of algebra #

Author: Chris Hughes

instance Complex.isAlgClosed :
IsAlgClosed ℂ

docs, source

Q193286: Rolle's theorem #

Author: Yury G. Kudryashov

theorem exists_deriv_eq_zero {f : ℝ → ℝ} {a b : ℝ} (hab : a < b) (hfc : ContinuousOn f (Set.Icc a b)) (hfI : f a = f b) :
∃ c ∈ Set.Ioo a b, deriv f c = 0

docs, source

Q193878: Chinese remainder theorem #
noncomputable def Ideal.quotientInfRingEquivPiQuotient {R : Type u} [CommRing R] {ι : Type u_1} [Finite ι] (f : ι → Ideal R) (hf : Pairwise (Function.onFun IsCoprime f)) :
R ⧸ ⨅ (i : ι), f i ≃+* ((i : ι) → R ⧸ f i)

docs, source

Q200787: Gödel's incompleteness theorem #

Author: Shogo Saito

url

Q203565: Solutions of a general cubic equation #

Author: Jeoff Lee

theorem Theorems100.cubic_eq_zero_iff {K : Type u_1} [Field K] (a b c d : K) {ω p q r s t : K} [Invertible 2] [Invertible 3] (ha : a ≠ 0) (hω : IsPrimitiveRoot ω 3) (hp : p = (3 * a * c - b ^ 2) / (9 * a ^ 2)) (hp_nonzero : p ≠ 0) (hq : q = (9 * a * b * c - 2 * b ^ 3 - 27 * a ^ 2 * d) / (54 * a ^ 3)) (hr : r ^ 2 = q ^ 2 + p ^ 3) (hs3 : s ^ 3 = q + r) (ht : t * s = p) (x : K) :
a * x ^ 3 + b * x ^ 2 + c * x + d = 0 ↔ x = s - t - b / (3 * a) ∨ x = s * ω - t * ω ^ 2 - b / (3 * a) ∨ x = s * ω ^ 2 - t * ω - b / (3 * a)

docs, source

Q208416: Independence of the continuum hypothesis #

Authors: Floris van Doorn and Jesse Michael Han

url

Q220680: Banach fixed-point theorem #
theorem ContractingWith.exists_fixedPoint {α : Type u_1} [EMetricSpace α] {K : NNReal} {f : α → α} [CompleteSpace α] (hf : ContractingWith K f) (x : α) (hx : edist x (f x) ≠ ⊤) :
∃ (y : α), Function.IsFixedPt f y ∧ Filter.Tendsto (fun (n : ℕ) => f^[n] x) Filter.atTop (nhds y) ∧ ∀ (n : ℕ), edist (f^[n] x) y ≤ edist x (f x) * ↑K ^ n / (1 - ↑K)

docs, source

Q245098: Intermediate value theorem #

Authors: Rob Lewis and Chris Hughes

theorem intermediate_value_Icc {α : Type u} [ConditionallyCompleteLinearOrder α] [TopologicalSpace α] [OrderTopology α] [DenselyOrdered α] {δ : Type u_1} [LinearOrder δ] [TopologicalSpace δ] [OrderClosedTopology δ] {a b : α} (hab : a ≤ b) {f : α → δ} (hf : ContinuousOn f (Set.Icc a b)) :
Set.Icc (f a) (f b) ⊆ f '' Set.Icc a b

docs, source

Q253214: Heine–Borel theorem #
theorem Metric.isCompact_iff_isClosed_bounded {α : Type u} [PseudoMetricSpace α] {s : Set α} [T2Space α] [ProperSpace α] :
IsCompact s ↔ IsClosed s ∧ Bornology.IsBounded s

docs, source

theorem FiniteDimensional.proper (𝕜 : Type u) [NontriviallyNormedField 𝕜] (E : Type v) [NormedAddCommGroup E] [NormedSpace 𝕜 E] [LocallyCompactSpace 𝕜] [FiniteDimensional 𝕜 E] :
ProperSpace E

docs, source

Q257387: Vitali theorem #

Author: Ching-Tsun Chou

url

mathlib4 pull request at https://github.com/leanprover-community/mathlib4/pull/20722

Q258374: Carathéodory's theorem #
def MeasureTheory.OuterMeasure.caratheodory {α : Type u} (m : MeasureTheory.OuterMeasure α) :
MeasurableSpace α

docs, source

Hard to say what exactly is meant.

Q276082: Wilson's theorem #

Author: Chris Hughes

theorem ZMod.wilsons_lemma (p : ℕ) [Fact (Nat.Prime p)] :
↑(p - 1).factorial = -1

docs, source

Q288465: Orbit-stabilizer theorem #
noncomputable def MulAction.orbitEquivQuotientStabilizer (α : Type u) {β : Type v} [Group α] [MulAction α β] (b : β) :
↑(MulAction.orbit α b) ≃ α ⧸ MulAction.stabilizer α b

docs, source

Q303402: Rank–nullity theorem #
theorem LinearMap.rank_range_add_rank_ker {R : Type u_1} {M M₁ : Type u} [Ring R] [AddCommGroup M] [AddCommGroup M₁] [Module R M] [Module R M₁] [HasRankNullity.{u, u_1} R] (f : M →ₗ[R] M₁) :
Module.rank R ↥(LinearMap.range f) + Module.rank R ↥(LinearMap.ker f) = Module.rank R M

docs, source

Q318767: Abel's theorem #

Author: Jeremy Tan

theorem Complex.tendsto_tsum_powerSeries_nhdsWithin_stolzCone {f : ℕ → ℂ} {l : ℂ} (h : Filter.Tendsto (fun (n : ℕ) => ∑ i ∈ Finset.range n, f i) Filter.atTop (nhds l)) {s : ℝ} (hs : 0 < s) :
Filter.Tendsto (fun (z : ℂ) => ∑' (n : ℕ), f n * z ^ n) (nhdsWithin 1 (Complex.stolzCone s)) (nhds l)

docs, source

theorem Real.tendsto_tsum_powerSeries_nhdsWithin_lt {f : ℕ → ℝ} {l : ℝ} (h : Filter.Tendsto (fun (n : ℕ) => ∑ i ∈ Finset.range n, f i) Filter.atTop (nhds l)) :
Filter.Tendsto (fun (x : ℝ) => ∑' (n : ℕ), f n * x ^ n) (nhdsWithin 1 (Set.Iio 1)) (nhds l)

docs, source

Q420714: Akra–Bazzi theorem #
theorem AkraBazziRecurrence.isBigO_asympBound {α : Type u_1} [Fintype α] {T : ℕ → ℝ} {g : ℝ → ℝ} {a b : α → ℝ} {r : α → ℕ → ℕ} [Nonempty α] (R : AkraBazziRecurrence T g a b r) :
T =O[Filter.atTop] AkraBazziRecurrence.asympBound g a b

docs, source

Q422187: Myhill–Nerode theorem #

Author: Chris Wong

theorem Language.isRegular_iff_finite_range_leftQuotient {α : Type u} {L : Language α} :
L.IsRegular ↔ (Set.range L.leftQuotient).Finite

docs, source

Q459547: Ptolemy's theorem #

Author: Manuel Candales

theorem EuclideanGeometry.mul_dist_add_mul_dist_eq_mul_dist_of_cospherical {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] {P : Type u_2} [MetricSpace P] [NormedAddTorsor V P] {a b c d p : P} (h : EuclideanGeometry.Cospherical {a, b, c, d}) (hapc : EuclideanGeometry.angle a p c = Real.pi) (hbpd : EuclideanGeometry.angle b p d = Real.pi) :
dist a b * dist c d + dist b c * dist d a = dist a c * dist b d

docs, source

Q468391: Bolzano–Weierstrass theorem #
theorem tendsto_subseq_of_frequently_bounded {X : Type u_1} [PseudoMetricSpace X] [ProperSpace X] {s : Set X} (hs : Bornology.IsBounded s) {x : ℕ → X} (hx : ∃ᶠ (n : ℕ) in Filter.atTop, x n ∈ s) :
∃ a ∈ closure s, ∃ (φ : ℕ → ℕ), StrictMono φ ∧ Filter.Tendsto (x ∘ φ) Filter.atTop (nhds a)

docs, source

theorem tendsto_subseq_of_bounded {X : Type u_1} [PseudoMetricSpace X] [ProperSpace X] {s : Set X} (hs : Bornology.IsBounded s) {x : ℕ → X} (hx : ∀ (n : ℕ), x n ∈ s) :
∃ a ∈ closure s, ∃ (φ : ℕ → ℕ), StrictMono φ ∧ Filter.Tendsto (x ∘ φ) Filter.atTop (nhds a)

docs, source

Q470877: Stirling's theorem #

Authors: Moritz Firsching and Fabian Kruse and Nikolas Kuhn and Heather Macbeth

theorem Stirling.tendsto_stirlingSeq_sqrt_pi :
Filter.Tendsto Stirling.stirlingSeq Filter.atTop (nhds √Real.pi)

docs, source

Q472883: Quadratic reciprocity theorem #

Authors: Chris Hughes (first) and Michael Stoll (second)

theorem legendreSym.quadratic_reciprocity {p q : ℕ} [Fact (Nat.Prime p)] [Fact (Nat.Prime q)] (hp : p ≠ 2) (hq : q ≠ 2) (hpq : p ≠ q) :
legendreSym q ↑p * legendreSym p ↑q = (-1) ^ (p / 2 * (q / 2))

docs, source

theorem jacobiSym.quadratic_reciprocity {a b : ℕ} (ha : Odd a) (hb : Odd b) :
jacobiSym (↑a) b = (-1) ^ (a / 2 * (b / 2)) * jacobiSym (↑b) a

docs, source

Q474881: Cantor's theorem #

Authors: Johannes Hölzl and Mario Carneiro

theorem Function.cantor_surjective {α : Type u_4} (f : α → Set α) :
¬Function.Surjective f

docs, source

Q476776: Solutions of a general quartic equation #

Author: Thomas Zhu

theorem Theorems100.quartic_eq_zero_iff {K : Type u_1} [Field K] (a b c d e : K) {p q r s u v w : K} [Invertible 2] (ha : a ≠ 0) (hp : p = (8 * a * c - 3 * b ^ 2) / (8 * a ^ 2)) (hq : q = (b ^ 3 - 4 * a * b * c + 8 * a ^ 2 * d) / (8 * a ^ 3)) (hq_nonzero : q ≠ 0) (hr : r = (16 * a * b ^ 2 * c + 256 * a ^ 3 * e - 3 * b ^ 4 - 64 * a ^ 2 * b * d) / (256 * a ^ 4)) (hu : u ^ 3 - p * u ^ 2 - 4 * r * u + 4 * p * r - q ^ 2 = 0) (hs : s ^ 2 = u - p) (hv : v ^ 2 = 4 * s ^ 2 - 8 * (u - q / s)) (hw : w ^ 2 = 4 * s ^ 2 - 8 * (u + q / s)) (x : K) :
a * x ^ 4 + b * x ^ 3 + c * x ^ 2 + d * x + e = 0 ↔ x = (-2 * s - v) / 4 - b / (4 * a) ∨ x = (-2 * s + v) / 4 - b / (4 * a) ∨ x = (2 * s - w) / 4 - b / (4 * a) ∨ x = (2 * s + w) / 4 - b / (4 * a)

docs, source

Q505798: Lagrange's theorem #
theorem Subgroup.card_subgroup_dvd_card {α : Type u_1} [Group α] (s : Subgroup α) :
Nat.card ↥s ∣ Nat.card α

docs, source

Q530152: Picard–Lindelöf theorem #
theorem IsPicardLindelof.exists_forall_hasDerivWithinAt_Icc_eq {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {v : ℝ → E → E} {tMin t₀ tMax : ℝ} (x₀ : E) {C R : ℝ} {L : NNReal} (hpl : IsPicardLindelof v tMin t₀ tMax x₀ L R C) :
∃ (f : ℝ → E), f t₀ = x₀ ∧ ∀ t ∈ Set.Icc tMin tMax, HasDerivWithinAt f (v t (f t)) (Set.Icc tMin tMax) t

docs, source

Q536640: Hall's marriage theorem #
theorem Finset.all_card_le_biUnion_card_iff_exists_injective {ι : Type u} {α : Type v} [DecidableEq α] (t : ι → Finset α) :
(∀ (s : Finset ι), s.card ≤ (s.biUnion t).card) ↔ ∃ (f : ι → α), Function.Injective f ∧ ∀ (x : ι), f x ∈ t x

docs, source

Q537618: Banach–Alaoglu theorem #
theorem WeakDual.isCompact_polar (𝕜 : Type u_1) [NontriviallyNormedField 𝕜] {E : Type u_2} [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [ProperSpace 𝕜] {s : Set E} (s_nhd : s ∈ nhds 0) :
IsCompact (WeakDual.polar 𝕜 s)

docs, source

Q550402: Dirichlet's theorem on arithmetic progressions #

Author: David Loeffler, Michael Stoll

theorem Nat.setOf_prime_and_eq_mod_infinite {q : ℕ} [NeZero q] {a : ZMod q} (ha : IsUnit a) :
{p : ℕ | Nat.Prime p ∧ ↑p = a}.Infinite

docs, source

Q570779: Vieta's formulas #
theorem Multiset.prod_X_add_C_eq_sum_esymm {R : Type u_1} [CommSemiring R] (s : Multiset R) :
(Multiset.map (fun (r : R) => Polynomial.X + Polynomial.C r) s).prod = ∑ j ∈ Finset.range (s.card + 1), Polynomial.C (s.esymm j) * Polynomial.X ^ (s.card - j)

docs, source

Q576478: Liouville's theorem #
theorem Differentiable.apply_eq_apply_of_bounded {E : Type u} [NormedAddCommGroup E] [NormedSpace ℂ E] {F : Type v} [NormedAddCommGroup F] [NormedSpace ℂ F] {f : E → F} (hf : Differentiable ℂ f) (hb : Bornology.IsBounded (Set.range f)) (z w : E) :
f z = f w

docs, source

Q609612: Knaster–Tarski theorem #

Author: Kenny Lau

instance fixedPoints.completeLattice {α : Type u} [CompleteLattice α] (f : α →o α) :
CompleteLattice ↑(Function.fixedPoints ⇑f)

docs, source

Q619985: Multinomial theorem #
theorem Finset.sum_pow_eq_sum_piAntidiag_of_commute {α : Type u_1} {R : Type u_2} [DecidableEq α] [Semiring R] (s : Finset α) (f : α → R) (hc : (↑s).Pairwise (Function.onFun Commute f)) (n : ℕ) :
(∑ i ∈ s, f i) ^ n = ∑ k ∈ s.piAntidiag n, ↑(Nat.multinomial s k) * s.noncommProd (fun (i : α) => f i ^ k i) ⋯

docs, source

Q632546: Bertrand's postulate #

Authors: Bolton Bailey and Patrick Stevens

theorem Nat.bertrand (n : ℕ) (hn0 : n ≠ 0) :
∃ (p : ℕ), Nat.Prime p ∧ n < p ∧ p ≤ 2 * n

docs, source

Q642620: Krein–Milman theorem #

Author: Yaël Dillies

theorem closure_convexHull_extremePoints {E : Type u_1} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] [T2Space E] [TopologicalAddGroup E] [ContinuousSMul ℝ E] [LocallyConvexSpace ℝ E] {s : Set E} (hscomp : IsCompact s) (hAconv : Convex ℝ s) :
closure ((convexHull ℝ) (Set.extremePoints ℝ s)) = s

docs, source

Q656772: Cayley–Hamilton theorem #

Author: Kim Morrison

theorem Matrix.aeval_self_charpoly {R : Type u_1} [CommRing R] {n : Type u_4} [DecidableEq n] [Fintype n] (M : Matrix n n R) :
(Polynomial.aeval M) M.charpoly = 0

docs, source

Q657482: Abel–Ruffini theorem #

Author: Thomas Browning

theorem AbelRuffini.exists_not_solvable_by_rad :
∃ (x : ℂ), IsAlgebraic ℚ x ∧ ¬IsSolvableByRad ℚ x

docs, source

Q670235: Fundamental theorem of arithmetic #

Author: Chris Hughes

theorem Nat.primeFactorsList_unique {n : ℕ} {l : List ℕ} (h₁ : l.prod = n) (h₂ : ∀ p ∈ l, Nat.Prime p) :
l.Perm n.primeFactorsList

docs, source

instance Int.euclideanDomain :
EuclideanDomain ℤ

docs, source

instance EuclideanDomain.to_principal_ideal_domain {R : Type u} [EuclideanDomain R] :
IsPrincipalIdealRing R

docs, source

class UniqueFactorizationMonoid (α : Type u_2) [CancelCommMonoidWithZero α] extends IsWellFounded α DvdNotUnit :
Prop

docs, source

theorem UniqueFactorizationMonoid.factors_unique {α : Type u_1} [CancelCommMonoidWithZero α] [UniqueFactorizationMonoid α] {f g : Multiset α} (hf : ∀ x ∈ f, Irreducible x) (hg : ∀ x ∈ g, Irreducible x) (h : Associated f.prod g.prod) :
Multiset.Rel Associated f g

docs, source

it also has a generalized version, by showing that every Euclidean domain is a unique factorization domain, and showing that the integers form a Euclidean domain.

Q716171: Erdős–Ginzburg–Ziv theorem #

Author: Yaël Dillies

theorem ZMod.erdos_ginzburg_ziv {ι : Type u_1} {n : ℕ} {s : Finset ι} (a : ι → ZMod n) (hs : 2 * n - 1 ≤ s.card) :
∃ t ⊆ s, t.card = n ∧ ∑ i ∈ t, a i = 0

docs, source

Q718875: Erdős–Ko–Rado theorem #

Author: Bhavik Mehta, Yaël Dillies

theorem Finset.erdos_ko_rado {n : ℕ} {𝒜 : Finset (Finset (Fin n))} {r : ℕ} (h𝒜 : (↑𝒜).Intersecting) (h₂ : Set.Sized r ↑𝒜) (h₃ : r ≤ n / 2) :
𝒜.card ≤ (n - 1).choose (r - 1)

docs, source

Q720469: Chevalley–Warning theorem #

Author: Johan Commelin

theorem char_dvd_card_solutions_of_sum_lt {K : Type u_1} {σ : Type u_2} {ι : Type u_3} [Fintype K] [Field K] [Fintype σ] [DecidableEq σ] [DecidableEq K] (p : ℕ) [CharP K p] {s : Finset ι} {f : ι → MvPolynomial σ K} (h : ∑ i ∈ s, (f i).totalDegree < Fintype.card σ) :
p ∣ Fintype.card { x : σ → K // ∀ i ∈ s, (MvPolynomial.eval x) (f i) = 0 }

docs, source

Q748233: Sylvester–Gallai theorem #

Author: Bhavik Mehta

url

Q752375: Extreme value theorem #

Author: Sébastien Gouëzel

theorem IsCompact.exists_isMinOn {α : Type u_2} {β : Type u_3} [LinearOrder α] [TopologicalSpace α] [TopologicalSpace β] [ClosedIicTopology α] {s : Set β} (hs : IsCompact s) (ne_s : s.Nonempty) {f : β → α} (hf : ContinuousOn f s) :
∃ x ∈ s, IsMinOn f s x

docs, source

Q756946: Lagrange's four-square theorem #

Author: Chris Hughes

theorem Nat.sum_four_squares (n : ℕ) :
∃ (a : ℕ) (b : ℕ) (c : ℕ) (d : ℕ), a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2 = n

docs, source

Q764287: Van der Waerden's theorem #

Author: David Wärn

theorem Combinatorics.exists_mono_homothetic_copy {M : Type u_5} {κ : Type u_6} [AddCommMonoid M] (S : Finset M) [Finite κ] (C : M → κ) :
∃ a > 0, ∃ (b : M) (c : κ), ∀ s ∈ S, C (a • s + b) = c

docs, source

Q765987: Heine–Cantor theorem #
theorem CompactSpace.uniformContinuous_of_continuous {α : Type u_1} {β : Type u_2} [UniformSpace α] [UniformSpace β] [CompactSpace α] {f : α → β} (h : Continuous f) :
UniformContinuous f

docs, source

Q834025: Cauchy integral theorem #

Author: Yury Kudryashov

theorem Complex.circleIntegral_div_sub_of_differentiable_on_off_countable {R : ℝ} {c w : ℂ} {s : Set ℂ} (hs : s.Countable) (hw : w ∈ Metric.ball c R) {f : ℂ → ℂ} (hc : ContinuousOn f (Metric.closedBall c R)) (hd : ∀ z ∈ Metric.ball c R \ s, DifferentiableAt ℂ f z) :
(∮ (z : ℂ) in C(c, R), f z / (z - w)) = 2 * ↑Real.pi * Complex.I * f w

docs, source

Q837506: Theorem on friends and strangers #

Author: Bhavik Mehta

url

will enter mathlib in 2024

Q842953: Lebesgue's density theorem #

Author: Oliver Nash

theorem Besicovitch.ae_tendsto_measure_inter_div {β : Type u} [MetricSpace β] [MeasurableSpace β] [BorelSpace β] [SecondCountableTopology β] [HasBesicovitchCovering β] (μ : MeasureTheory.Measure β) [MeasureTheory.IsLocallyFiniteMeasure μ] (s : Set β) :
∀ᵐ (x : β) ∂μ.restrict s, Filter.Tendsto (fun (r : ℝ) => μ (s ∩ Metric.closedBall x r) / μ (Metric.closedBall x r)) (nhdsWithin 0 (Set.Ioi 0)) (nhds 1)

docs, source

Q848375: Implicit function theorem #
def ImplicitFunctionData.implicitFunction {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [CompleteSpace E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] [CompleteSpace F] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace 𝕜 G] [CompleteSpace G] (φ : ImplicitFunctionData 𝕜 E F G) :
F → G → E

docs, source

Q853067: Solutions to Pell's equation #

Author: Mario Carneiro (first), Michael Stoll (second)

theorem Pell.eq_pell {a : ℕ} (a1 : 1 < a) {x y : ℕ} (hp : x * x - Pell.d✝ a1 * y * y = 1) :
∃ (n : ℕ), x = Pell.xn a1 n ∧ y = Pell.yn a1 n

docs, source

theorem Pell.exists_of_not_isSquare {d : ℤ} (h₀ : 0 < d) (hd : ¬IsSquare d) :
∃ (x : ℤ) (y : ℤ), x ^ 2 - d * y ^ 2 = 1 ∧ y ≠ 0

docs, source

In pell.eq_pell, d is defined to be a*a - 1 for an arbitrary a > 1.

Q866116: Hahn–Banach theorem #
theorem exists_extension_norm_eq {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] [IsRCLikeNormedField 𝕜] {E : Type u_2} [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] (p : Subspace 𝕜 E) (f : ↥p →L[𝕜] 𝕜) :
∃ (g : E →L[𝕜] 𝕜), (∀ (x : ↥p), g ↑x = f x) ∧ ‖g‖ = ‖f‖

docs, source

Q914517: Fermat's theorem on sums of two squares #

Author: Chris Hughes

theorem Nat.Prime.sq_add_sq {p : ℕ} [Fact (Nat.Prime p)] (hp : p % 4 ≠ 3) :
∃ (a : ℕ) (b : ℕ), a ^ 2 + b ^ 2 = p

docs, source

Q918099: Ramsey's theorem #

Author: Bhavik Mehta

url

Q931001: Inverse function theorem #
theorem HasStrictFDerivAt.to_localInverse {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} {f' : E ≃L[𝕜] F} {a : E} [CompleteSpace E] (hf : HasStrictFDerivAt f (↑f') a) :
HasStrictFDerivAt (HasStrictFDerivAt.localInverse f f' a hf) (↑f'.symm) (f a)

docs, source

Q939927: Stone–Weierstrass theorem #

Authors: Scott Morrison and Heather Macbeth

theorem ContinuousMap.subalgebra_topologicalClosure_eq_top_of_separatesPoints {X : Type u_1} [TopologicalSpace X] [CompactSpace X] (A : Subalgebra ℝ C(X, ℝ)) (w : A.SeparatesPoints) :
A.topologicalClosure = ⊤

docs, source

Q943246: Wedderburn's little theorem #
instance littleWedderburn (D : Type u_1) [DivisionRing D] [Finite D] :
Field D

docs, source

Q948664: Kneser's addition theorem #

Author: Mantas Bakšys, Yaël Dillies

url

Q967972: Open mapping theorem #
theorem AnalyticOnNhd.is_constant_or_isOpen {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {U : Set E} {g : E → ℂ} (hg : AnalyticOnNhd ℂ g U) (hU : IsPreconnected U) :
(∃ (w : ℂ), ∀ z ∈ U, g z = w) ∨ ∀ s ⊆ U, IsOpen s → IsOpen (g '' s)

docs, source

Q976607: Erdős–Szekeres theorem #

Author: Bhavik Mehta

theorem Theorems100.erdos_szekeres {α : Type u_1} [LinearOrder α] {r s n : ℕ} {f : Fin n → α} (hn : r * s < n) (hf : Function.Injective f) :
(∃ (t : Finset (Fin n)), r < t.card ∧ StrictMonoOn f ↑t) ∨ ∃ (t : Finset (Fin n)), s < t.card ∧ StrictAntiOn f ↑t

docs, source

Q1032886: Hales–Jewett theorem #

Author: David Wärn

theorem Combinatorics.Line.exists_mono_in_high_dimension (α : Type u) [Finite α] (κ : Type v) [Finite κ] :
∃ (ι : Type) (x : Fintype ι), ∀ (C : (ι → α) → κ), ∃ (l : Combinatorics.Line α ι), Combinatorics.Line.IsMono C l

docs, source

Q1033910: Cantor–Bernstein–Schroeder theorem #

Author: Mario Carneiro

theorem Function.Embedding.schroeder_bernstein {α : Type u} {β : Type v} {f : α → β} {g : β → α} (hf : Function.Injective f) (hg : Function.Injective g) :
∃ (h : α → β), Function.Bijective h

docs, source

Q1038716: Identity theorem #
theorem AnalyticOnNhd.eqOn_of_preconnected_of_frequently_eq {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {f g : 𝕜 → E} {z₀ : 𝕜} {U : Set 𝕜} (hf : AnalyticOnNhd 𝕜 f U) (hg : AnalyticOnNhd 𝕜 g U) (hU : IsPreconnected U) (h₀ : z₀ ∈ U) (hfg : ∃ᶠ (z : 𝕜) in nhdsWithin z₀ {z₀}ᶜ, f z = g z) :
Set.EqOn f g U

docs, source

Q1047749: Turán's theorem #

Author: Jeremy Tan

theorem SimpleGraph.isTuranMaximal_iff_nonempty_iso_turanGraph {V : Type u_1} [Fintype V] {G : SimpleGraph V} [DecidableRel G.Adj] {r : ℕ} (hr : 0 < r) :
G.IsTuranMaximal r ↔ Nonempty (G ≃g SimpleGraph.turanGraph (Fintype.card V) r)

docs, source

Q1050203: Cantor's intersection theorem #
theorem IsCompact.nonempty_sInter_of_directed_nonempty_isCompact_isClosed {X : Type u} [TopologicalSpace X] {S : Set (Set X)} [hS : Nonempty ↑S] (hSd : DirectedOn (fun (x1 x2 : Set X) => x1 ⊇ x2) S) (hSn : ∀ U ∈ S, U.Nonempty) (hSc : ∀ U ∈ S, IsCompact U) (hScl : ∀ U ∈ S, IsClosed U) :
(⋂₀ S).Nonempty

docs, source

Q1050932: Hartogs's theorem #

Author: Geoffrey Irving

url

Q1052678: Baire category theorem #
theorem dense_sInter_of_isOpen {X : Type u_1} [TopologicalSpace X] [BaireSpace X] {S : Set (Set X)} (ho : ∀ s ∈ S, IsOpen s) (hS : S.Countable) (hd : ∀ s ∈ S, Dense s) :
Dense (⋂₀ S)

docs, source

Q1057919: Sylow theorems #
theorem Sylow.exists_subgroup_card_pow_prime {G : Type u} [Group G] [Finite G] (p : ℕ) {n : ℕ} [Fact (Nat.Prime p)] (hdvd : p ^ n ∣ Nat.card G) :
∃ (K : Subgroup G), Nat.card ↥K = p ^ n

docs, source

instance Sylow.isPretransitive_of_finite {p : ℕ} {G : Type u_1} [Group G] [hp : Fact (Nat.Prime p)] [Finite (Sylow p G)] :
MulAction.IsPretransitive G (Sylow p G)

docs, source

theorem Sylow.card_dvd_index {p : ℕ} {G : Type u_1} [Group G] [Fact (Nat.Prime p)] [Finite (Sylow p G)] (P : Sylow p G) :
Nat.card (Sylow p G) ∣ (↑P).index

docs, source

theorem card_sylow_modEq_one (p : ℕ) (G : Type u_1) [Group G] [Fact (Nat.Prime p)] [Finite (Sylow p G)] :
Nat.card (Sylow p G) ≡ 1 [MOD p]

docs, source

Q1065257: Squeeze theorem #
theorem tendsto_of_tendsto_of_tendsto_of_le_of_le' {α : Type u} {β : Type v} [TopologicalSpace α] [Preorder α] [OrderTopology α] {f g h : β → α} {b : Filter β} {a : α} (hg : Filter.Tendsto g b (nhds a)) (hh : Filter.Tendsto h b (nhds a)) (hgf : ∀ᶠ (b : β) in b, g b ≤ f b) (hfh : ∀ᶠ (b : β) in b, f b ≤ h b) :
Filter.Tendsto f b (nhds a)

docs, source

Q1065966: Isomorphism theorem #
noncomputable def QuotientGroup.quotientKerEquivRange {G : Type u} [Group G] {H : Type v} [Group H] (φ : G →* H) :
G ⧸ φ.ker ≃* ↥φ.range

docs, source

noncomputable def QuotientGroup.quotientInfEquivProdNormalQuotient {G : Type u} [Group G] (H N : Subgroup G) [N.Normal] :
↥H ⧸ N.subgroupOf H ≃* ↥(H ⊔ N) ⧸ N.subgroupOf (H ⊔ N)

docs, source

def QuotientGroup.quotientQuotientEquivQuotient {G : Type u} [Group G] (N : Subgroup G) [nN : N.Normal] (M : Subgroup G) [nM : M.Normal] (h : N ≤ M) :
(G ⧸ N) ⧸ Subgroup.map (QuotientGroup.mk' N) M ≃* G ⧸ M

docs, source

Q1067156: Dominated convergence theorem #
theorem MeasureTheory.tendsto_integral_of_dominated_convergence {α : Type u_1} {G : Type u_3} [NormedAddCommGroup G] [NormedSpace ℝ G] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {F : ℕ → α → G} {f : α → G} (bound : α → ℝ) (F_measurable : ∀ (n : ℕ), MeasureTheory.AEStronglyMeasurable (F n) μ) (bound_integrable : MeasureTheory.Integrable bound μ) (h_bound : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, ‖F n a‖ ≤ bound a) (h_lim : ∀ᵐ (a : α) ∂μ, Filter.Tendsto (fun (n : ℕ) => F n a) Filter.atTop (nhds (f a))) :
Filter.Tendsto (fun (n : ℕ) => ∫ (a : α), F n a ∂μ) Filter.atTop (nhds (∫ (a : α), f a ∂μ))

docs, source

Q1067156X: Bounded convergence theorem #
theorem MeasureTheory.FiniteMeasure.tendsto_lintegral_nn_of_le_const {Ω : Type u_1} [MeasurableSpace Ω] [TopologicalSpace Ω] [OpensMeasurableSpace Ω] (μ : MeasureTheory.FiniteMeasure Ω) {fs : ℕ → BoundedContinuousFunction Ω NNReal} {c : NNReal} (fs_le_const : ∀ (n : ℕ) (ω : Ω), (fs n) ω ≤ c) {f : Ω → NNReal} (fs_lim : ∀ (ω : Ω), Filter.Tendsto (fun (n : ℕ) => (fs n) ω) Filter.atTop (nhds (f ω))) :
Filter.Tendsto (fun (n : ℕ) => ∫⁻ (ω : Ω), ↑((fs n) ω) ∂↑μ) Filter.atTop (nhds (∫⁻ (ω : Ω), ↑(f ω) ∂↑μ))

docs, source

theorem MeasureTheory.tendsto_lintegral_nn_filter_of_le_const {Ω : Type u_1} [TopologicalSpace Ω] [MeasurableSpace Ω] [OpensMeasurableSpace Ω] {ι : Type u_2} {L : Filter ι} [L.IsCountablyGenerated] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsFiniteMeasure μ] {fs : ι → BoundedContinuousFunction Ω NNReal} {c : NNReal} (fs_le_const : ∀ᶠ (i : ι) in L, ∀ᵐ (ω : Ω) ∂μ, (fs i) ω ≤ c) {f : Ω → NNReal} (fs_lim : ∀ᵐ (ω : Ω) ∂μ, Filter.Tendsto (fun (i : ι) => (fs i) ω) L (nhds (f ω))) :
Filter.Tendsto (fun (i : ι) => ∫⁻ (ω : Ω), ↑((fs i) ω) ∂μ) L (nhds (∫⁻ (ω : Ω), ↑(f ω) ∂μ))

docs, source

Q1068085: Closed graph theorem #
theorem LinearMap.continuous_of_isClosed_graph {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [CompleteSpace E] {F : Type u_5} [NormedAddCommGroup F] [NormedSpace 𝕜 F] [CompleteSpace F] (g : E →ₗ[𝕜] F) (hg : IsClosed ↑g.graph) :
Continuous ⇑g

docs, source

Q1068283: Löwenheim–Skolem theorem #
theorem FirstOrder.Language.exists_elementaryEmbedding_card_eq (L : FirstOrder.Language) (M : Type w') [L.Structure M] [iM : Infinite M] (κ : Cardinal.{w}) (h1 : Cardinal.aleph0 ≤ κ) (h2 : Cardinal.lift.{w, max u v} L.card ≤ Cardinal.lift.{max u v, w} κ) :
∃ (N : CategoryTheory.Bundled L.Structure), (Nonempty (L.ElementaryEmbedding (↑N) M) ∨ Nonempty (L.ElementaryEmbedding M ↑N)) ∧ Cardinal.mk ↑N = κ

docs, source

Q1068976: Hilbert's Nullstellensatz #
theorem MvPolynomial.vanishingIdeal_zeroLocus_eq_radical {k : Type u_1} [Field k] {σ : Type u_2} [IsAlgClosed k] [Finite σ] (I : Ideal (MvPolynomial σ k)) :
MvPolynomial.vanishingIdeal (MvPolynomial.zeroLocus I) = I.radical

docs, source

Q1082910: Euler's partition theorem #

Authors: Bhavik Mehta and Aaron Anderson

theorem Theorems100.partition_theorem (n : ℕ) :
(Nat.Partition.odds n).card = (Nat.Partition.distincts n).card

docs, source

Q1097021: Minkowski's theorem #

Authors: Alex J. Best and Yaël Dillies

theorem MeasureTheory.exists_ne_zero_mem_lattice_of_measure_mul_two_pow_lt_measure {E : Type u_1} [MeasurableSpace E] {μ : MeasureTheory.Measure E} {F s : Set E} [NormedAddCommGroup E] [NormedSpace ℝ E] [BorelSpace E] [FiniteDimensional ℝ E] [μ.IsAddHaarMeasure] {L : AddSubgroup E} [Countable ↥L] (fund : MeasureTheory.IsAddFundamentalDomain (↥L) F μ) (h_symm : ∀ x ∈ s, -x ∈ s) (h_conv : Convex ℝ s) (h : μ F * 2 ^ Module.finrank ℝ E < μ s) :
∃ (x : ↥L), x ≠ 0 ∧ ↑x ∈ s

docs, source

Q1137014: Tychonoff's theorem #
theorem isCompact_pi_infinite {ι : Type u_1} {X : ι → Type u_2} [(i : ι) → TopologicalSpace (X i)] {s : (i : ι) → Set (X i)} :
(∀ (i : ι), IsCompact (s i)) → IsCompact {x : (i : ι) → X i | ∀ (i : ι), x i ∈ s i}

docs, source

Q1137206: Taylor's theorem #

Author: Moritz Doll

theorem taylor_mean_remainder_lagrange {f : ℝ → ℝ} {x x₀ : ℝ} {n : ℕ} (hx : x₀ < x) (hf : ContDiffOn ℝ (↑n) f (Set.Icc x₀ x)) (hf' : DifferentiableOn ℝ (iteratedDerivWithin n f (Set.Icc x₀ x)) (Set.Ioo x₀ x)) :
∃ x' ∈ Set.Ioo x₀ x, f x - taylorWithinEval f n (Set.Icc x₀ x) x₀ x = iteratedDerivWithin (n + 1) f (Set.Icc x₀ x) x' * (x - x₀) ^ (n + 1) / ↑(n + 1).factorial

docs, source

theorem taylor_mean_remainder_cauchy {f : ℝ → ℝ} {x x₀ : ℝ} {n : ℕ} (hx : x₀ < x) (hf : ContDiffOn ℝ (↑n) f (Set.Icc x₀ x)) (hf' : DifferentiableOn ℝ (iteratedDerivWithin n f (Set.Icc x₀ x)) (Set.Ioo x₀ x)) :
∃ x' ∈ Set.Ioo x₀ x, f x - taylorWithinEval f n (Set.Icc x₀ x) x₀ x = iteratedDerivWithin (n + 1) f (Set.Icc x₀ x) x' * (x - x') ^ n / ↑n.factorial * (x - x₀)

docs, source

Q1139041: Cauchy's theorem #
theorem exists_prime_orderOf_dvd_card {G : Type u_3} [Group G] [Fintype G] (p : ℕ) [hp : Fact (Nat.Prime p)] (hdvd : p ∣ Fintype.card G) :
∃ (x : G), orderOf x = p

docs, source

Q1144897: Brouwer fixed-point theorem #

Author: Brendan Seamas Murphy

url

in Lean 3

Q1149022: Fubini's theorem #
theorem MeasureTheory.integral_prod {α : Type u_1} {β : Type u_2} {E : Type u_3} [MeasurableSpace α] [MeasurableSpace β] {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β} [NormedAddCommGroup E] [MeasureTheory.SFinite ν] [NormedSpace ℝ E] [MeasureTheory.SFinite μ] (f : α × β → E) (hf : MeasureTheory.Integrable f (μ.prod ν)) :
∫ (z : α × β), f z ∂μ.prod ν = ∫ (x : α), ∫ (y : β), f (x, y) ∂ν ∂μ

docs, source

Q1149458: Compactness theorem #
theorem FirstOrder.Language.Theory.isSatisfiable_iff_isFinitelySatisfiable {L : FirstOrder.Language} {T : L.Theory} :
T.IsSatisfiable ↔ T.IsFinitelySatisfiable

docs, source

Q1153584: Monotone convergence theorem #
theorem MeasureTheory.integral_tendsto_of_tendsto_of_antitone {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : ℕ → α → ℝ} {F : α → ℝ} (hf : ∀ (n : ℕ), MeasureTheory.Integrable (f n) μ) (hF : MeasureTheory.Integrable F μ) (h_mono : ∀ᵐ (x : α) ∂μ, Antitone fun (n : ℕ) => f n x) (h_tendsto : ∀ᵐ (x : α) ∂μ, Filter.Tendsto (fun (n : ℕ) => f n x) Filter.atTop (nhds (F x))) :
Filter.Tendsto (fun (n : ℕ) => ∫ (x : α), f n x ∂μ) Filter.atTop (nhds (∫ (x : α), F x ∂μ))

docs, source

theorem MeasureTheory.lintegral_tendsto_of_tendsto_of_monotone {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : ℕ → α → ENNReal} {F : α → ENNReal} (hf : ∀ (n : ℕ), AEMeasurable (f n) μ) (h_mono : ∀ᵐ (x : α) ∂μ, Monotone fun (n : ℕ) => f n x) (h_tendsto : ∀ᵐ (x : α) ∂μ, Filter.Tendsto (fun (n : ℕ) => f n x) Filter.atTop (nhds (F x))) :
Filter.Tendsto (fun (n : ℕ) => ∫⁻ (x : α), f n x ∂μ) Filter.atTop (nhds (∫⁻ (x : α), F x ∂μ))

docs, source

Q1186808: Lucas's theorem #
theorem Choose.lucas_theorem {n k p : ℕ} [Fact (Nat.Prime p)] {a : ℕ} (ha₁ : n < p ^ a) (ha₂ : k < p ^ a) :
↑(n.choose k) ≡ ∏ i ∈ Finset.range a, ↑((n / p ^ i % p).choose (k / p ^ i % p)) [ZMOD ↑p]

docs, source

Q1187646: Fundamental theorem on homomorphisms #
noncomputable def QuotientGroup.quotientKerEquivRange {G : Type u} [Group G] {H : Type v} [Group H] (φ : G →* H) :
G ⧸ φ.ker ≃* ↥φ.range

docs, source

Q1188392: Zeckendorf's theorem #
def Nat.zeckendorfEquiv :
ℕ ≃ { l : List ℕ // l.IsZeckendorfRep }

docs, source

Q1191319: Radon–Nikodym theorem #
theorem MeasureTheory.Measure.absolutelyContinuous_iff_withDensity_rnDeriv_eq {α : Type u_1} {m : MeasurableSpace α} {μ ν : MeasureTheory.Measure α} [μ.HaveLebesgueDecomposition ν] :
μ.AbsolutelyContinuous ν ↔ ν.withDensity (μ.rnDeriv ν) = μ

docs, source

Q1191709: Egorov's theorem #

Author: Kexing Ying

theorem MeasureTheory.tendstoUniformlyOn_of_ae_tendsto {α : Type u_1} {β : Type u_2} {ι : Type u_3} {m : MeasurableSpace α} [MetricSpace β] {μ : MeasureTheory.Measure α} [SemilatticeSup ι] [Nonempty ι] [Countable ι] {f : ι → α → β} {g : α → β} {s : Set α} (hf : ∀ (n : ι), MeasureTheory.StronglyMeasurable (f n)) (hg : MeasureTheory.StronglyMeasurable g) (hsm : MeasurableSet s) (hs : μ s ≠ ⊤) (hfg : ∀ᵐ (x : α) ∂μ, x ∈ s → Filter.Tendsto (fun (n : ι) => f n x) Filter.atTop (nhds (g x))) {ε : ℝ} (hε : 0 < ε) :
∃ t ⊆ s, MeasurableSet t ∧ μ t ≤ ENNReal.ofReal ε ∧ TendstoUniformlyOn f g Filter.atTop (s \ t)

docs, source

Q1194053: Metrization theorems #
instance TopologicalSpace.metrizableSpace_of_t3_secondCountable (X : Type u_1) [TopologicalSpace X] [T3Space X] [SecondCountableTopology X] :
TopologicalSpace.MetrizableSpace X

docs, source

Urysohn's metrization theorem (only)

Q1217677: Fundamental theorem of calculus #

Authors: Yury G. Kudryashov (first) and Benjamin Davidson (second)

theorem intervalIntegral.integral_hasStrictDerivAt_of_tendsto_ae_right {E : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {f : ℝ → E} {c : E} {a b : ℝ} (hf : IntervalIntegrable f MeasureTheory.volume a b) (hmeas : StronglyMeasurableAtFilter f (nhds b) MeasureTheory.volume) (hb : Filter.Tendsto f (nhds b ⊓ MeasureTheory.ae MeasureTheory.volume) (nhds c)) :
HasStrictDerivAt (fun (u : ℝ) => ∫ (x : ℝ) in a..u, f x) c b

docs, source

theorem intervalIntegral.integral_eq_sub_of_hasDeriv_right_of_le {E : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] {a b : ℝ} [CompleteSpace E] {f f' : ℝ → E} (hab : a ≤ b) (hcont : ContinuousOn f (Set.Icc a b)) (hderiv : ∀ x ∈ Set.Ioo a b, HasDerivWithinAt f (f' x) (Set.Ioi x) x) (f'int : IntervalIntegrable f' MeasureTheory.volume a b) :
∫ (y : ℝ) in a..b, f' y = f b - f a

docs, source

Q1243340: Birkhoff–Von Neumann theorem #

Author: Bhavik Mehta

theorem doublyStochastic_eq_convexHull_permMatrix {R : Type u_1} {n : Type u_2} [Fintype n] [DecidableEq n] [LinearOrderedField R] :
↑(doublyStochastic R n) = (convexHull R) {x : Matrix n n R | ∃ (σ : Equiv.Perm n), Equiv.Perm.permMatrix R σ = x}

docs, source

Q1259814: Nielsen–Schreier theorem #
instance subgroupIsFreeOfIsFree {G : Type u} [Group G] [IsFreeGroup G] (H : Subgroup G) :
IsFreeGroup ↥H

docs, source

Q1306095: Whitney embedding theorem #
theorem exists_embedding_euclidean_of_compact {E : Type uE} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {H : Type uH} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type uM} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I (↑⊤) M] [T2Space M] [CompactSpace M] :
∃ (n : ℕ) (e : M → EuclideanSpace ℝ (Fin n)), ContMDiff I (modelWithCornersSelf ℝ (EuclideanSpace ℝ (Fin n))) (↑⊤) e ∧ Topology.IsClosedEmbedding e ∧ ∀ (x : M), Function.Injective ⇑(mfderiv I (modelWithCornersSelf ℝ (EuclideanSpace ℝ (Fin n))) e x)

docs, source

baby version: for compact manifolds; embedding into some n

Q1346677: Tietze extension theorem #
theorem BoundedContinuousFunction.exists_extension_norm_eq_of_isClosedEmbedding {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [NormalSpace Y] (f : BoundedContinuousFunction X ℝ) {e : X → Y} (he : Topology.IsClosedEmbedding e) :
∃ (g : BoundedContinuousFunction Y ℝ), ‖g‖ = ‖f‖ ∧ ⇑g ∘ e = ⇑f

docs, source

Q1426292: Banach–Steinhaus theorem #

Author: Jireh Loreaux

theorem banach_steinhaus {E : Type u_1} {F : Type u_2} {𝕜 : Type u_3} {𝕜₂ : Type u_4} [SeminormedAddCommGroup E] [SeminormedAddCommGroup F] [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜₂] [NormedSpace 𝕜 E] [NormedSpace 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} [RingHomIsometric σ₁₂] {ι : Type u_5} [CompleteSpace E] {g : ι → E →SL[σ₁₂] F} (h : ∀ (x : E), ∃ (C : ℝ), ∀ (i : ι), ‖(g i) x‖ ≤ C) :
∃ (C' : ℝ), ∀ (i : ι), ‖g i‖ ≤ C'

docs, source

Q1477053: Arzelà–Ascoli theorem #
theorem BoundedContinuousFunction.arzela_ascoli {α : Type u} {β : Type v} [TopologicalSpace α] [CompactSpace α] [PseudoMetricSpace β] [T2Space β] (s : Set β) (hs : IsCompact s) (A : Set (BoundedContinuousFunction α β)) (in_s : ∀ (f : BoundedContinuousFunction α β) (x : α), f ∈ A → f x ∈ s) (H : Equicontinuous fun (x : ↑A) => ⇑↑x) :
IsCompact (closure A)

docs, source

Q1506253: Euclid's theorem #

Author: Jeremy Avigad

theorem Nat.exists_infinite_primes (n : ℕ) :
∃ (p : ℕ), n ≤ p ∧ Nat.Prime p

docs, source

Q1542114: Bézout's theorem #

Author: mathlib

theorem Nat.gcd_eq_gcd_ab (x y : ℕ) :
↑(x.gcd y) = ↑x * x.gcdA y + ↑y * x.gcdB y

docs, source

Q1566341: Hindman's theorem #

Author: David Wärn

theorem Hindman.FP_partition_regular {M : Type u_1} [Semigroup M] (a : Stream' M) (s : Set (Set M)) (sfin : s.Finite) (scov : Hindman.FP a ⊆ ⋃₀ s) :
∃ c ∈ s, ∃ (b : Stream' M), Hindman.FP b ⊆ c

docs, source

Q1568811: Hahn decomposition theorem #

Author: Kexing Ying

theorem MeasureTheory.SignedMeasure.exists_isCompl_positive_negative {α : Type u_1} [MeasurableSpace α] (s : MeasureTheory.SignedMeasure α) :
∃ (i : Set α) (j : Set α), MeasurableSet i ∧ MeasureTheory.VectorMeasure.restrict 0 i ≤ MeasureTheory.VectorMeasure.restrict s i ∧ MeasurableSet j ∧ MeasureTheory.VectorMeasure.restrict s j ≤ MeasureTheory.VectorMeasure.restrict 0 j ∧ IsCompl i j

docs, source

Q1632433: Helly's theorem #

Author: Vasily Nesterov

theorem Convex.helly_theorem {ι : Type u_1} {𝕜 : Type u_2} {E : Type u_3} [LinearOrderedField 𝕜] [AddCommGroup E] [Module 𝕜 E] [FiniteDimensional 𝕜 E] {F : ι → Set E} {s : Finset ι} (h_card : Module.finrank 𝕜 E + 1 ≤ s.card) (h_convex : ∀ i ∈ s, Convex 𝕜 (F i)) (h_inter : ∀ I ⊆ s, I.card = Module.finrank 𝕜 E + 1 → (⋂ i ∈ I, F i).Nonempty) :
(⋂ i ∈ s, F i).Nonempty

docs, source

Q1687147: Sprague–Grundy theorem #

Author: Fox Thomson

theorem SetTheory.PGame.equiv_nim_grundyValue (G : SetTheory.PGame) [G.Impartial] :
G ≈ SetTheory.PGame.nim (Nimber.toOrdinal G.grundyValue)

docs, source

Q1752621: Sylvester's law of inertia #
theorem QuadraticForm.equivalent_one_zero_neg_one_weighted_sum_squared {M : Type u_2} [AddCommGroup M] [Module ℝ M] [FiniteDimensional ℝ M] (Q : QuadraticForm ℝ M) :
∃ (w : Fin (Module.finrank ℝ M) → ℝ), (∀ (i : Fin (Module.finrank ℝ M)), w i = -1 ∨ w i = 0 ∨ w i = 1) ∧ QuadraticMap.Equivalent Q (QuadraticMap.weightedSumSquares ℝ w)

docs, source

Q1816952: Schur's lemma #
theorem CategoryTheory.finrank_endomorphism_simple_eq_one {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Preadditive C] (𝕜 : Type u_2) [Field 𝕜] [IsAlgClosed 𝕜] [CategoryTheory.Linear 𝕜 C] [CategoryTheory.Limits.HasKernels C] (X : C) [CategoryTheory.Simple X] [FiniteDimensional 𝕜 (X ⟶ X)] :
Module.finrank 𝕜 (X ⟶ X) = 1

docs, source

Q1893717: Rice's theorem #
theorem ComputablePred.rice (C : Set (ℕ →. ℕ)) (h : ComputablePred fun (c : Nat.Partrec.Code) => c.eval ∈ C) {f g : ℕ →. ℕ} (hf : Nat.Partrec f) (hg : Nat.Partrec g) (fC : f ∈ C) :
g ∈ C

docs, source

Q2027347: Optional stopping theorem #

Author: Kexing Ying, Rémy Degenne

theorem MeasureTheory.submartingale_iff_expected_stoppedValue_mono {Ω : Type u_1} {m0 : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {𝒢 : MeasureTheory.Filtration ℕ m0} {f : ℕ → Ω → ℝ} [MeasureTheory.IsFiniteMeasure μ] (hadp : MeasureTheory.Adapted 𝒢 f) (hint : ∀ (i : ℕ), MeasureTheory.Integrable (f i) μ) :
MeasureTheory.Submartingale f 𝒢 μ ↔ ∀ (τ π : Ω → ℕ), MeasureTheory.IsStoppingTime 𝒢 τ → MeasureTheory.IsStoppingTime 𝒢 π → τ ≤ π → (∃ (N : ℕ), ∀ (x : Ω), π x ≤ N) → ∫ (x : Ω), MeasureTheory.stoppedValue f τ x ∂μ ≤ ∫ (x : Ω), MeasureTheory.stoppedValue f π x ∂μ

docs, source

Q2093886: Primitive element theorem #
theorem Field.exists_primitive_element (F : Type u_1) (E : Type u_2) [Field F] [Field E] [Algebra F E] [FiniteDimensional F E] [Algebra.IsSeparable F E] :
∃ (α : E), F⟮α⟯ = ⊤

docs, source

Q2226786: Sperner's theorem #

Author: Bhavik Mehta, Alena Gusakov, Yaël Dillies

theorem IsAntichain.sperner {α : Type u_2} [Fintype α] {𝒜 : Finset (Finset α)} (h𝒜 : IsAntichain (fun (x1 x2 : Finset α) => x1 ⊆ x2) ↑𝒜) :
𝒜.card ≤ (Fintype.card α).choose (Fintype.card α / 2)

docs, source

Q2226800: Schur–Zassenhaus theorem #

Author: Thomas Browning

theorem Subgroup.exists_left_complement'_of_coprime {G : Type u} [Group G] {N : Subgroup G} [N.Normal] (hN : (Nat.card ↥N).Coprime N.index) :
∃ (H : Subgroup G), H.IsComplement' N

docs, source

Q2226855: Sharkovskii's theorem #

Author: Bhavik Mehta

Q2253746: Bertrand's ballot theorem #

Authors: Bhavik Mehta and Kexing Ying

theorem Ballot.ballot_problem (q p : ℕ) :
q < p → (ProbabilityTheory.uniformOn (Ballot.countedSequence p q)) Ballot.staysPositive = (↑p - ↑q) / (↑p + ↑q)

docs, source

Q2275191: Lebesgue differentiation theorem #

Author: Sébastien Gouëzel

theorem VitaliFamily.ae_tendsto_lintegral_div {α : Type u_1} [PseudoMetricSpace α] {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} (v : VitaliFamily μ) [SecondCountableTopology α] [BorelSpace α] [MeasureTheory.IsLocallyFiniteMeasure μ] {f : α → ENNReal} (hf : AEMeasurable f μ) (h'f : ∫⁻ (y : α), f y ∂μ ≠ ⊤) :
∀ᵐ (x : α) ∂μ, Filter.Tendsto (fun (a : Set α) => (∫⁻ (y : α) in a, f y ∂μ) / μ a) (v.filterAt x) (nhds (f x))

docs, source

Q2471737: Carathéodory's theorem #
theorem convexHull_eq_union {𝕜 : Type u_1} {E : Type u} [LinearOrderedField 𝕜] [AddCommGroup E] [Module 𝕜 E] {s : Set E} :
(convexHull 𝕜) s = ⋃ (t : Finset E), ⋃ (_ : ↑t ⊆ s), ⋃ (_ : AffineIndependent 𝕜 Subtype.val), (convexHull 𝕜) ↑t

docs, source

Q2525646: Jordan–Hölder theorem #
theorem CompositionSeries.jordan_holder {X : Type u} [Lattice X] [JordanHolderLattice X] (s₁ s₂ : CompositionSeries X) (hb : RelSeries.head s₁ = RelSeries.head s₂) (ht : RelSeries.last s₁ = RelSeries.last s₂) :
s₁.Equivalent s₂

docs, source

Q2919401: Ostrowski's theorem #

Author: David Kurniadi Angdinata, Fabrizio Barroero, Laura Capuano, Nirvana Coppola, María Inés de Frutos-Fernández, Sam van Gool, Silvain Rideau-Kikuchi, Amos Turchet, Francesco Veneziano

theorem Rat.AbsoluteValue.equiv_real_or_padic (f : AbsoluteValue ℚ ℝ) (hf_nontriv : f.IsNontrivial) :
f ≈ Rat.AbsoluteValue.real ∨ ∃! p : ℕ, ∃ (x : Fact (Nat.Prime p)), f ≈ Rat.AbsoluteValue.padic p

docs, source

Q3229352: Vitali covering theorem #

Author: Sébastien Gouëzel

theorem Vitali.exists_disjoint_covering_ae {α : Type u_1} {ι : Type u_2} [PseudoMetricSpace α] [MeasurableSpace α] [OpensMeasurableSpace α] [SecondCountableTopology α] (μ : MeasureTheory.Measure α) [MeasureTheory.IsLocallyFiniteMeasure μ] (s : Set α) (t : Set ι) (C : NNReal) (r : ι → ℝ) (c : ι → α) (B : ι → Set α) (hB : ∀ a ∈ t, B a ⊆ Metric.closedBall (c a) (r a)) (μB : ∀ a ∈ t, μ (Metric.closedBall (c a) (3 * r a)) ≤ ↑C * μ (B a)) (ht : ∀ a ∈ t, (interior (B a)).Nonempty) (h't : ∀ a ∈ t, IsClosed (B a)) (hf : ∀ x ∈ s, ∀ ε > 0, ∃ a ∈ t, r a ≤ ε ∧ c a = x) :
∃ u ⊆ t, u.Countable ∧ u.PairwiseDisjoint B ∧ μ (s \ ⋃ a ∈ u, B a) = 0

docs, source

Q3526996: Kolmogorov extension theorem #

Author: Rémy Degenne, Peter Pfaffelhuber

url

Q3527102: Kruskal–Katona theorem #

Author: Bhavik Mehta, Yaël Dillies

theorem Finset.kruskal_katona {n r : ℕ} {𝒜 𝒞 : Finset (Finset (Fin n))} (h𝒜r : Set.Sized r ↑𝒜) (h𝒞𝒜 : 𝒞.card ≤ 𝒜.card) (h𝒞 : Finset.Colex.IsInitSeg 𝒞 r) :
𝒞.shadow.card ≤ 𝒜.shadow.card

docs, source

Q3527118: Mahler's theorem #
theorem PadicInt.hasSum_mahler {p : ℕ} [hp : Fact (Nat.Prime p)] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℚ_[p] E] [IsUltrametricDist E] [CompleteSpace E] (f : C(ℤ_[p], E)) :
HasSum (fun (n : ℕ) => PadicInt.mahlerTerm ((fwdDiff 1)^[n] (⇑f) 0) n) f

docs, source

Q3527189: Lattice theorem #
def QuotientGroup.quotientQuotientEquivQuotient {G : Type u} [Group G] (N : Subgroup G) [nN : N.Normal] (M : Subgroup G) [nM : M.Normal] (h : N ≤ M) :
(G ⧸ N) ⧸ Subgroup.map (QuotientGroup.mk' N) M ≃* G ⧸ M

docs, source

Q3527205: Dimension theorem for vector spaces #
theorem mk_eq_mk_of_basis {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] [Module R M] {ι : Type w} {ι' : Type w'} [InvariantBasisNumber R] (v : Basis ι R M) (v' : Basis ι' R M) :
Cardinal.lift.{w', w} (Cardinal.mk ι) = Cardinal.lift.{w, w'} (Cardinal.mk ι')

docs, source

Q3527215: Hilbert projection theorem #

Author: Zhouhang Zhou

theorem exists_norm_eq_iInf_of_complete_convex {F : Type u_3} [NormedAddCommGroup F] [InnerProductSpace ℝ F] {K : Set F} (ne : K.Nonempty) (h₁ : IsComplete K) (h₂ : Convex ℝ K) (u : F) :
∃ v ∈ K, ‖u - v‖ = ⨅ (w : ↑K), ‖u - ↑w‖

docs, source

Q3527250: Hadamard three-lines theorem #

Author: Xavier Généreux

theorem Complex.HadamardThreeLines.norm_le_interpStrip_of_mem_verticalClosedStrip {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] (f : ℂ → E) {z : ℂ} (hz : z ∈ Complex.HadamardThreeLines.verticalClosedStrip 0 1) (hd : DiffContOnCl ℂ f (Complex.HadamardThreeLines.verticalStrip 0 1)) (hB : BddAbove (norm ∘ f '' Complex.HadamardThreeLines.verticalClosedStrip 0 1)) :
‖f z‖ ≤ ‖Complex.HadamardThreeLines.interpStrip f z‖

docs, source

Q3527263: Kleene fixed-point theorem #

Author: Ira Fesefeldt

theorem fixedPoints.lfp_eq_sSup_iterate {α : Type u} [CompleteLattice α] (f : α →o α) (h : OmegaCompletePartialOrder.ωScottContinuous ⇑f) :
OrderHom.lfp f = ⨆ (n : ℕ), (⇑f)^[n] ⊥

docs, source

Q3984053: Fourier inversion theorem #

Author: Sébastien Gouëzel

theorem Continuous.fourier_inversion {V : Type u_1} {E : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MeasurableSpace V] [BorelSpace V] [FiniteDimensional ℝ V] [NormedAddCommGroup E] [NormedSpace ℂ E] {f : V → E} [CompleteSpace E] (h : Continuous f) (hf : MeasureTheory.Integrable f MeasureTheory.volume) (h'f : MeasureTheory.Integrable (Real.fourierIntegral f) MeasureTheory.volume) :
Real.fourierIntegralInv (Real.fourierIntegral f) = f

docs, source

Q4378868: Phragmén–Lindelöf theorem #

Author: Yury G. Kudryashov

theorem PhragmenLindelof.horizontal_strip {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {a b C : ℝ} {f : ℂ → E} {z : ℂ} (hfd : DiffContOnCl ℂ f (Complex.im ⁻¹' Set.Ioo a b)) (hB : ∃ c < Real.pi / (b - a), ∃ (B : ℝ), f =O[Filter.comap (abs ∘ Complex.re) Filter.atTop ⊓ Filter.principal (Complex.im ⁻¹' Set.Ioo a b)] fun (z : ℂ) => Real.exp (B * Real.exp (c * |z.re|))) (hle_a : ∀ (z : ℂ), z.im = a → ‖f z‖ ≤ C) (hle_b : ∀ (z : ℂ), z.im = b → ‖f z‖ ≤ C) (hza : a ≤ z.im) (hzb : z.im ≤ b) :
‖f z‖ ≤ C

docs, source

Q4695203: Four functions theorem #

Author: Yaël Dillies

theorem four_functions_theorem {α : Type u_1} {β : Type u_2} [DistribLattice α] [LinearOrderedCommSemiring β] [ExistsAddOfLE β] (f₁ f₂ f₃ f₄ : α → β) [DecidableEq α] (h₁ : 0 ≤ f₁) (h₂ : 0 ≤ f₂) (h₃ : 0 ≤ f₃) (h₄ : 0 ≤ f₄) (h : ∀ (a b : α), f₁ a * f₂ b ≤ f₃ (a ⊓ b) * f₄ (a ⊔ b)) (s t : Finset α) :
(∑ a ∈ s, f₁ a) * ∑ a ∈ t, f₂ a ≤ (∑ a ∈ s ⊼ t, f₃ a) * ∑ a ∈ s ⊻ t, f₄ a

docs, source

Q4830725: Ax–Grothendieck theorem #

Author: Chris Hughes

theorem ax_grothendieck_zeroLocus {K : Type u_1} {ι : Type u_2} [Field K] [IsAlgClosed K] [Finite ι] (I : Ideal (MvPolynomial ι K)) (p : ι → MvPolynomial ι K) :
let S := MvPolynomial.zeroLocus I; Set.MapsTo (fun (v : ι → K) (i : ι) => (MvPolynomial.eval v) (p i)) S S → Set.InjOn (fun (v : ι → K) (i : ι) => (MvPolynomial.eval v) (p i)) S → Set.SurjOn (fun (v : ι → K) (i : ι) => (MvPolynomial.eval v) (p i)) S S

docs, source

Q5171652: Corners theorem #

Author: Yaël Dillies, Bhavik Mehta

theorem corners_theorem_nat {n : ℕ} {ε : ℝ} (hε : 0 < ε) (hn : cornersTheoremBound (ε / 9) ≤ n) (A : Finset (ℕ × ℕ)) (hAn : A ⊆ Finset.range n ×ˢ Finset.range n) (hAε : ε * ↑n ^ 2 ≤ ↑A.card) :
¬IsCornerFree ↑A

docs, source

Q5437947: Fatou–Lebesgue theorem #
theorem MeasureTheory.lintegral_liminf_le {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : ℕ → α → ENNReal} (h_meas : ∀ (n : ℕ), Measurable (f n)) :
∫⁻ (a : α), Filter.liminf (fun (n : ℕ) => f n a) Filter.atTop ∂μ ≤ Filter.liminf (fun (n : ℕ) => ∫⁻ (a : α), f n a ∂μ) Filter.atTop

docs, source

Q5504427: Friendship theorem #

Authors: Aaron Anderson and Jalex Stark and Kyle Miller

theorem Theorems100.friendship_theorem {V : Type u} [Fintype V] {G : SimpleGraph V} (hG : Theorems100.Friendship G) [Nonempty V] :
Theorems100.ExistsPolitician G

docs, source

Q6757284: Marcinkiewicz theorem #

Author: Jim Portegies

url

Q6813106: Mellin inversion theorem #
theorem mellin_inversion {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E] (σ : ℝ) (f : ℝ → E) {x : ℝ} (hx : 0 < x) (hf : MellinConvergent f ↑σ) (hFf : Complex.VerticalIntegrable (mellin f) σ MeasureTheory.volume) (hfx : ContinuousAt f x) :
mellinInv σ (mellin f) x = f x

docs, source

Q7432915: Schroeder–Bernstein theorem for measurable spaces #
noncomputable def MeasurableEmbedding.schroederBernstein {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] {f : α → β} {g : β → α} (hf : MeasurableEmbedding f) (hg : MeasurableEmbedding g) :
α ≃ᵐ β

docs, source

Q7433182: Schwartz–Zippel theorem #

Author: Bolton Bailey, Yaël Dillies

theorem MvPolynomial.schwartz_zippel_sup_sum {R : Type u_1} [CommRing R] [IsDomain R] [DecidableEq R] {n : ℕ} {p : MvPolynomial (Fin n) R} (hp : p ≠ 0) (S : Fin n → Finset R) :
↑(Finset.filter (fun (x : Fin n → R) => (MvPolynomial.eval x) p = 0) (Fintype.piFinset fun (i : Fin n) => S i)).card / ∏ i : Fin n, ↑(S i).card ≤ p.support.sup fun (s : Fin n →₀ ℕ) => ∑ i : Fin n, ↑(s i) / ↑(S i).card

docs, source

Q7820874: Tonelli's theorem #
theorem MeasureTheory.lintegral_prod {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β} [MeasureTheory.SFinite ν] (f : α × β → ENNReal) (hf : AEMeasurable f (μ.prod ν)) :
∫⁻ (z : α × β), f z ∂μ.prod ν = ∫⁻ (x : α), ∫⁻ (y : β), f (x, y) ∂ν ∂μ

docs, source

Q7888360: Structure theorem for finitely generated modules over a principal ideal domain #

Author: Pierre-Alexandre Bazin

theorem Module.equiv_free_prod_directSum {R : Type u} [CommRing R] [IsPrincipalIdealRing R] {N : Type (max u v)} [AddCommGroup N] [Module R N] [IsDomain R] [h' : Module.Finite R N] :
∃ (n : ℕ) (ι : Type u) (x : Fintype ι) (p : ι → R) (_ : ∀ (i : ι), Irreducible (p i)) (e : ι → ℕ), Nonempty (N ≃ₗ[R] (Fin n →₀ R) × DirectSum ι fun (i : ι) => R ⧸ Submodule.span R {p i ^ e i})

docs, source

Q8074796: Zsigmondy's theorem #

Author: Mantas Bakšys

Q9993851: Lax–Milgram theorem #
def IsCoercive.continuousLinearEquivOfBilin {V : Type u} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [CompleteSpace V] {B : V →L[ℝ] V →L[ℝ] ℝ} (coercive : IsCoercive B) :
V ≃L[ℝ] V

docs, source

Q11352023: Vitali convergence theorem #

Author: Igor Khavkine

theorem MeasureTheory.tendstoInMeasure_iff_tendsto_Lp {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} [NormedAddCommGroup β] {μ : MeasureTheory.Measure α} {p : ENNReal} {f : ℕ → α → β} {g : α → β} (hp : 1 ≤ p) (hp' : p ≠ ⊤) (hf : ∀ (n : ℕ), MeasureTheory.Memℒp (f n) p μ) (hg : MeasureTheory.Memℒp g p μ) :
MeasureTheory.TendstoInMeasure μ f Filter.atTop g ∧ MeasureTheory.UnifIntegrable f p μ ∧ MeasureTheory.UnifTight f p μ ↔ Filter.Tendsto (fun (n : ℕ) => MeasureTheory.eLpNorm (f n - g) p μ) Filter.atTop (nhds 0)

docs, source

Q16251580: Matiyasevich's theorem #

Author: Mario Carneiro

theorem Pell.matiyasevic {a k x y : ℕ} :
(∃ (a1 : 1 < a), Pell.xn a1 k = x ∧ Pell.yn a1 k = y) ↔ 1 < a ∧ k ≤ y ∧ (x = 1 ∧ y = 0 ∨ ∃ (u : ℕ) (v : ℕ) (s : ℕ) (t : ℕ) (b : ℕ), x * x - (a * a - 1) * y * y = 1 ∧ u * u - (a * a - 1) * v * v = 1 ∧ s * s - (b * b - 1) * t * t = 1 ∧ 1 < b ∧ b ≡ 1 [MOD 4 * y] ∧ b ≡ a [MOD u] ∧ 0 < v ∧ y * y ∣ v ∧ s ≡ x [MOD u] ∧ t ≡ k [MOD 4 * y])

docs, source

Q17005116: Birkhoff's representation theorem #

Author: Yaël Dillies

noncomputable def LatticeHom.birkhoffSet {α : Type u_1} [DistribLattice α] [Fintype α] [DecidablePred SupIrred] :
LatticeHom α (Set { a : α // SupIrred a })

docs, source

Q18206266: Euclid–Euler theorem #

Author: Aaron Anderson

theorem Theorems100.Nat.eq_two_pow_mul_prime_mersenne_of_even_perfect {n : ℕ} (ev : Even n) (perf : n.Perfect) :
∃ (k : ℕ), Nat.Prime (mersenne (k + 1)) ∧ n = 2 ^ k * mersenne (k + 1)

docs, source

Q22952648: Uncountability of the continuum #

Author: Floris van Doorn

theorem Cardinal.not_countable_real :
¬Set.univ.Countable

docs, source

The following theorems have just their statement formalized. Contributions to their proofs are welcome.
Q132469: Fermat's Last Theorem #
def FermatLastTheorem :
Prop

docs, source

Formalisation of the proof is on-going in https://imperialcollegelondon.github.io/FLT/.

Q776578: Artin–Wedderburn theorem #