Sets

StructureSet#

A set is a collection of elements of some type α.

To build a set (an element of Set α) out of a predicate p : α → Prop, use the set builder notation {a | p a}. To get a predicate α → Prop from a set s : Set α, use the ∈ notation, as in a ∈ s or (· ∈ s).

Set.{u} (α : Type u) : Type u
Sources
MathlibSet
Used by 27
Used bySchroeder-Bernstein Theorem · Cantor’s Theorem · Matching · Fixed points · Category · Grothendieck topology · Small category · Subfield · Group · Group action · Subgroup · Ideal of a commutative ring · Natural number · Ring · Subring · DFA · Language · NFA · \(\varepsilon\)-NFA · Cofinality · Hitting time · Filter · Topological space · Birkhoff's representation theorem · Boolean prime ideal theorem · Szpilrajn extension theorem · Orbit

StructureFinite set#

Finset α is the type of finite sets of elements of α. It is implemented as a multiset (a list up to permutation) which has no duplicate elements.

Finset.{u_3} (α : Type u_3) : Type u_3
Sources
MathlibFinset
Uses 1 · Used by 110
Statement usesMultiset
Used byEuler’s Generalization of Fermat’s Little Theorem · Formula for Pythagorean Triples · Arithmetic Mean/Geometric Mean · Divergence of the Harmonic Series · Königsberg Bridges Problem · Sum of the Reciprocals of the Triangular Numbers · The Binomial Theorem · The Number of Subsets of a Set · The Partition Theorem · Wilson’s Lemma · Ascending or Descending Sequences (Erdős–Szekeres Theorem) · Formula for the Number of Combinations · L’Hopital’s Rule · Sum of an arithmetic series · The Mean Value Theorem (Freek Wiedijk's 100 theorems) · The Perfect Number Theorem · Theorem of Ceva · Derangements Formula · Principle of Inclusion/Exclusion · The Friendship Theorem · Carathéodory's theorem · Jensen's inequality (finite sum version) · Derivative of a composition of functions (Analysis) · Derivative of the inverse of a function (Analysis) · Local extrema · Mean value theorem (Differentiability) · Eigenvalues from Rayleigh quotient · Hahn-Banach theorem · Isometric inclusion in double dual · Additive energy · Cauchy-Davenport theorem · Doubling constant · Dyson transform · Erdős–Ginzburg–Ziv theorem · Plünnecke-Petridis inequality · Ruzsa covering lemma · Ruzsa triangle inequality · Small tripling implies small powers · Bell numbers · Catalan numbers · Degree-sum formula · Strongly regular graphs · Triangle counting lemma · Turán's theorem · Finite · Infinite · Strong pigeonhole principle · Hales-Jewett theorem · Van der Waerden theorem · Ahlswede-Zhang identity · Four functions theorem · Harris-Kleitman inequality · Kleitman's theorem · Kruskal-Katona theorem · LYM inequality · Maximum size of an intersecting family · Sperner's theorem · VC dimension · Hall's marriage theorem · Finitely supported function · Barycenter · Existence of orthonormal basis · Finite-dimensionality · Noetherian module · In terms of Turing machines · Context-free grammar · Regular language · Compactness theorem · Compactness in terms of open covers (Borel-Lebesgue) · Arzela-Ascoli theorem · Infinite sum · Jacobson density theorem · Lasker–Noether theorem · Binomial inverse theorem · Birkhoff–Von Neumann theorem · Gershgorin circle theorem · Wedderburn–Artin theorem · Lie's theorem · Mitchell's embedding theorem · Cauchy's theorem (group theory) · Jordan–Hölder theorem · Darboux's theorem (analysis) · Euler's theorem on homogeneous functions · Erdős–Ko–Rado theorem · Multinomial theorem · Birkhoff's representation theorem · Cantor's isomorphism theorem · Radon's theorem · Fermat's little theorem · Glaisher's theorem · Lucas's theorem · Gram-Schmidt orthogonalisation · Decomposition into cycles with disjoint support · Signature · Direct sum · Gaussian elimination · Inverse function theorem (Differential calculus) · Partial derivatives commute · Cauchy-Lipschitz Theorem · Bézout's identity · Complex exponential · Radius of convergence · Derivative of a composition of functions (Single Variable Real Analysis) · Derivative of the inverse of a function (Single Variable Real Analysis) · Higher-order derivatives of functions · Leibniz formula (Single Variable Real Analysis) · Riemann sums · Alternating series · Norms \(\lVert\cdot\rVert_p\) on \(\R^n\) and \(\C^n\) · Finite product of metric spaces

DefinitionMultiset#

Multiset α is the quotient of List α by list permutation. The result is a type of finite sets with duplicates allowed.

Multiset.{u} (α : Type u) : Type u
Sources
MathlibMultiset
Uses 1 · Used by 5
Statement usesList
Used byThe Fundamental Theorem of Arithmetic · Freiman homomorphisms · Finite map · Finite set · Roots of a polynomial

DefinitionOrdered set#

An Ordset α is a finite set of values, represented as a tree. The operations on this type maintain that the tree is balanced and correctly stores subtree sizes at each level. The correctness property of the tree is baked into the type, so all operations on this type are correct by construction.

Ordset.{u_2} (α : Type u_2) [Preorder α] : Type u_2
Sources
MathlibOrdset
Uses 1
Statement usesSize-balanced binary search tree

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.