Definitions: Mathlib.Combinatorics, part 1 of 3

Behrend.boxdefMathlib.Combinatorics.Additive.AP.Three.Behrend, function or constant

Wording

no wording

English

Let $n$ and $d$ be natural numbers. Then $\operatorname{box}$ applied to $n$ and $d$ is a finite set of the set of functions from elements of $\mathrm{Fin}$ applied to $n$ to natural numbers defined as the product finite set of the function that maps $x$ to the range of $d$.

Behrend.dValuedefMathlib.Combinatorics.Additive.AP.Three.Behrend, function or constant

Wording

the value of N (from the name)

English

Let $N$ be a natural number. Then the value of $N$ is a natural number defined as the floor of the quotient of the exponentiation of $N$ to $\operatorname{inv}$ applied to the value of $N$ and $2$.

Behrend.mapdefMathlib.Combinatorics.Additive.AP.Three.Behrend, function or constant

Wording

the map of d (from the name)

English

Let $d$ be a natural number. Then the map of $d$ is an additive monoid homomorphism of the set of functions from elements of $\mathrm{Fin}$ applied to $n$ to natural numbers and $\Natural$.

Behrend.nValuedefMathlib.Combinatorics.Additive.AP.Three.Behrend, function or constant

Wording

the value of N (from the name)

English

Let $N$ be a natural number. Then the value of $N$ is a natural number defined as $\operatorname{ceil}$ applied to the square root of the logarithm of $N$.

Behrend.spheredefMathlib.Combinatorics.Additive.AP.Three.Behrend, function or constant

Wording

the sphere of d and k (from the name)

English

Let $n$, $d$ and $k$ be natural numbers. Then the sphere of $d$ and $k$ is a finite set of the set of functions from elements of $\mathrm{Fin}$ applied to $n$ to natural numbers defined as $\FinsetFilter {x}{\mathrm{Eq} (\FinsetSum {\FinsetunivMACRoAC}{i}{(x (i)^ {2})}, k)}{\operatorname{box} (n , d)}$.

Mathlib.Combinatorics.Additive.AP.Three.Defs

ThreeAPFreedefMathlib.Combinatorics.Additive.AP.Three.Defs, predicate

Wording

no wording

English

Let $s$ be an element of $\wp x$. Then $\mathrm{ThreeAPFree}$ holds for $s$, if for all elements $a$ of $x$, if $a$ is an element of $s$, then for all elements $b$ of $x$, if $b$ is an element of $s$, then for all elements $c$ of $x$, if $c$ is an element of $s$, then if $\EqtMACRoH {a + c}{b + b}$, then $\EqtMACRoH {a}{b}$.

ThreeGPFreedefMathlib.Combinatorics.Additive.AP.Three.Defs, predicate

Wording

no wording

English

Let $s$ be an element of $\wp x$. Then $\mathrm{ThreeGPFree}$ holds for $s$, if for all elements $a$ of $x$, if $a$ is an element of $s$, then for all elements $b$ of $x$, if $b$ is an element of $s$, then for all elements $c$ of $x$, if $c$ is an element of $s$, then if $\EqtMACRoH {a \times c}{b \times b}$, then $\EqtMACRoH {a}{b}$.

addRothNumberdefMathlib.Combinatorics.Additive.AP.Three.Defs, function or constant

Wording

no wording

English

$\mathrm{addRothNumber}$ is an order homomorphism of the set of finite sets of $x$ and $\Natural$.

mulRothNumberdefMathlib.Combinatorics.Additive.AP.Three.Defs, function or constant

Wording

no wording

English

$\mathrm{mulRothNumber}$ is an order homomorphism of the set of finite sets of $x$ and $\Natural$.

rothNumberNatdefMathlib.Combinatorics.Additive.AP.Three.Defs, function or constant

Wording

no wording

English

$\mathrm{rothNumberNat}$ is an order homomorphism of $\Natural$ and $\Natural$.

Mathlib.Combinatorics.Additive.ApproximateSubgroup

IsApproximateAddSubgroupstructureMathlib.Combinatorics.Additive.ApproximateSubgroup, predicate

Wording

no wording

English

Let $K$ be a real number. Let $A$ be an element of $\wp G$. Then we can say that $\mathrm{IsApproximateAddSubgroup}$ holds for $K$ and $A$.

IsApproximateSubgroupstructureMathlib.Combinatorics.Additive.ApproximateSubgroup, predicate

Wording

no wording

English

Let $K$ be a real number. Let $A$ be an element of $\wp G$. Then we can say that $\mathrm{IsApproximateSubgroup}$ holds for $K$ and $A$.

Mathlib.Combinatorics.Additive.Convolution

Finset.addConvolutiondefMathlib.Combinatorics.Additive.Convolution, function or constant

Wording

the additive convolution of B and x2 (from the name)

English

Let $A$ and $B$ be finite sets of $G$. Let $x_{2}$ be an element of $G$. Then the additive convolution of $B$ and $x_{2}$ is a natural number defined as the cardinality of $\FinsetFilter {\mathrm{ab}}{(\EqtMACRoH {(\ProdfstMACRoZ {\mathrm{ab}}+ \ProdsndMACRoAA {\mathrm{ab}})}{x_{2}})}{\operatorname{sprod} (A , B)}$.

Finset.convolutiondefMathlib.Combinatorics.Additive.Convolution, function or constant

Wording

the convolution of B and x2 (from the name)

English

Let $A$ and $B$ be finite sets of $G$. Let $x_{2}$ be an element of $G$. Then the convolution of $B$ and $x_{2}$ is a natural number defined as the cardinality of $\FinsetFilter {\mathrm{ab}}{(\EqtMACRoH {(\ProdfstMACRoZ {\mathrm{ab}}\times \ProdsndMACRoAA {\mathrm{ab}})}{x_{2}})}{\operatorname{sprod} (A , B)}$.

Mathlib.Combinatorics.Additive.Corner.Defs

IsCornerstructureMathlib.Combinatorics.Additive.Corner.Defs, predicate

Wording

no wording

English

Let $A$ be an element of $\wp \mathrm{Prod} (G , G)$. Let $x_{1}$, $x_{2}$, $x_{3}$ and $x_{4}$ be elements of $G$. Then we can say that $\mathrm{IsCorner}$ holds for $A$, $x_{1}$, $x_{2}$, $x_{3}$ and $x_{4}$.

IsCornerFreedefMathlib.Combinatorics.Additive.Corner.Defs, predicate

Wording

A is a corner free (from the name)

English

Let $A$ be an element of $\wp \mathrm{Prod} (G , G)$. Then $A$ is a corner free, if for all elements $x_{1}$, $x_{2}$, $x_{3}$ and $x_{4}$ of $G$, if $\mathrm{IsCorner}$ holds for $A$, $x_{1}$, $x_{2}$, $x_{3}$ and $x_{4}$, then $\EqtMACRoH {x_{1}}{x_{3}}$.

Mathlib.Combinatorics.Additive.Corner.Roth

cornersTheoremBounddefMathlib.Combinatorics.Additive.Corner.Roth, function or constant

Wording

the corner theorem bound of x (from the name)

English

Let $x$ be a real number. Then the corner theorem bound of $x$ is a natural number defined as the sum of the floor of $\operatorname{inv}$ applied to $\operatorname{triangleRemovalBound} (\frac{ x}{9})\times 27$ and $1$.

Mathlib.Combinatorics.Additive.CovBySMul

CovBySMuldefMathlib.Combinatorics.Additive.CovBySMul, predicate

Wording

no wording

English

Let $M$ be a set. Let $K$ be a real number. Let $A$ and $B$ be elements of $\wp X$. Then $\mathrm{CovBySMul}$ holds for $M$, $K$, $A$ and $B$, if there exists a finite set $F$ of $M$, such that $\FinsetcardMACRoM {F}\leq K$ and $A \leq \HSMulhSMulMACRoAL {F}{B}$.

CovByVAdddefMathlib.Combinatorics.Additive.CovBySMul, predicate

Wording

no wording

English

Let $M$ be a set. Let $K$ be a real number. Let $A$ and $B$ be elements of $\wp X$. Then $\mathrm{CovByVAdd}$ holds for $M$, $K$, $A$ and $B$, if there exists a finite set $F$ of $M$, such that $\FinsetcardMACRoM {F}\leq K$ and $A$ is less than or equal to the sum of $F$ and $B$.

Mathlib.Combinatorics.Additive.Dissociation

AddDissociateddefMathlib.Combinatorics.Additive.Dissociation, predicate

Wording

no wording

English

Let $s$ be an element of $\wp x$. Then $\mathrm{AddDissociated}$ holds for $s$, if the function that maps $x_{2}$ to $\FinsetSum {x_{2}}{x_{3}}{x_{3}}$ is injective on $\operatorname{ofPred}$ applied to the function that maps $t$ to $\mathrm{Leq} (t , s)$.

Finset.addSpandefMathlib.Combinatorics.Additive.Dissociation, function or constant

Wording

the span of s (from the docstring)

English

Let $s$ be a finite set of $x$. Then the span of $s$ is a finite set of $x$ defined as the forward image of the product finite set of the function that maps $\mathrm{\_a}$ to $\operatorname{insert}$ applied to $\operatorname{neg}$ applied to $1$ and $\operatorname{insert}$ applied to $0$ and $\operatorname{singleton}$ applied to $1$ under the function that maps $x_{4}$ to $\FinsetSum {s}{a}{(\HSMulhSMulMACRoAL {x_{4} (a)}{a})}$.

Finset.mulSpandefMathlib.Combinatorics.Additive.Dissociation, function or constant

Wording

the span of s (from the docstring)

English

MulDissociateddefMathlib.Combinatorics.Additive.Dissociation, predicate

Wording

no wording

English

Let $s$ be an element of $\wp x$. Then $\mathrm{MulDissociated}$ holds for $s$, if the function that maps $x_{2}$ to $\FinsetProd {x_{2}}{x_{3}}{x_{3}}$ is injective on $\operatorname{ofPred}$ applied to the function that maps $t$ to $\mathrm{Leq} (t , s)$.

Mathlib.Combinatorics.Additive.DoublingConst

Finset.addConstdefMathlib.Combinatorics.Additive.DoublingConst, function or constant

Wording

the doubling constant of A and B (from the docstring)

English

Let $A$ and $B$ be finite sets of $G$. Then the doubling constant of $A$ and $B$ is a nonnegative rational number defined as $\frac{ \FinsetcardMACRoM {(A + B)}}{\FinsetcardMACRoM {A}}$.

Finset.divConstdefMathlib.Combinatorics.Additive.DoublingConst, function or constant

Wording

the difference constant of A and B (from the docstring)

English

Let $A$ and $B$ be finite sets of $G$. Then the difference constant of $A$ and $B$ is a nonnegative rational number defined as $\frac{ \FinsetcardMACRoM {(\frac{ A}{B})}}{\FinsetcardMACRoM {A}}$.

Finset.mulConstdefMathlib.Combinatorics.Additive.DoublingConst, function or constant

Wording

the doubling constant of A and B (from the docstring)

English

Let $A$ and $B$ be finite sets of $G$. Then the doubling constant of $A$ and $B$ is a nonnegative rational number defined as $\frac{ \FinsetcardMACRoM {(A \times B)}}{\FinsetcardMACRoM {A}}$.

Finset.subConstdefMathlib.Combinatorics.Additive.DoublingConst, function or constant

Wording

the difference constant of A and B (from the docstring)

English

Let $A$ and $B$ be finite sets of $G$. Then the difference constant of $A$ and $B$ is a nonnegative rational number defined as $\frac{ \FinsetcardMACRoM {(A - B)}}{\FinsetcardMACRoM {A}}$.

Mathlib.Combinatorics.Additive.ETransform

Finset.addDysonETransformdefMathlib.Combinatorics.Additive.ETransform, function or constant

Wording

no wording

English

Let $e$ be an element of $x$. Let $x_{3}$ be an element of $\mathrm{Prod}$ applied to the set of finite sets of $x$ and the set of finite sets of $x$. Then $\operatorname{addDysonETransform}$ applied to $e$ and $x_{3}$ is an element of $\mathrm{Prod}$ applied to the set of finite sets of $x$ and the set of finite sets of $x$ defined as $\ProdmkMACRoU {(\UnionunionMACRoAB {\ProdfstMACRoZ {x_{3}}}{\operatorname{hVAdd} (e , \ProdsndMACRoAA {x_{3}})})}{\operatorname{inter} (\ProdsndMACRoAA {x_{3}}, \operatorname{hVAdd} (\operatorname{neg} (e), \ProdfstMACRoZ {x_{3}}))}$.

Finset.addETransformLeftdefMathlib.Combinatorics.Additive.ETransform, function or constant

Wording

the left additive transform of e and x3 (from the name)

English

Let $e$ be an element of $x$. Let $x_{3}$ be an element of $\mathrm{Prod}$ applied to the set of finite sets of $x$ and the set of finite sets of $x$. Then the left additive transform of $e$ and $x_{3}$ is an element of $\mathrm{Prod}$ applied to the set of finite sets of $x$ and the set of finite sets of $x$ defined as $\ProdmkMACRoU {\operatorname{inter} (\ProdfstMACRoZ {x_{3}}, \operatorname{hVAdd} (\operatorname{op} (e), \ProdfstMACRoZ {x_{3}}))}{(\UnionunionMACRoAB {\ProdsndMACRoAA {x_{3}}}{\operatorname{hVAdd} (\operatorname{neg} (e), \ProdsndMACRoAA {x_{3}})})}$.

Finset.addETransformRightdefMathlib.Combinatorics.Additive.ETransform, function or constant

Wording

the right additive transform of e and x3 (from the name)

English

Let $e$ be an element of $x$. Let $x_{3}$ be an element of $\mathrm{Prod}$ applied to the set of finite sets of $x$ and the set of finite sets of $x$. Then the right additive transform of $e$ and $x_{3}$ is an element of $\mathrm{Prod}$ applied to the set of finite sets of $x$ and the set of finite sets of $x$ defined as $\ProdmkMACRoU {(\UnionunionMACRoAB {\ProdfstMACRoZ {x_{3}}}{\operatorname{hVAdd} (\operatorname{op} (e), \ProdfstMACRoZ {x_{3}})})}{\operatorname{inter} (\ProdsndMACRoAA {x_{3}}, \operatorname{hVAdd} (\operatorname{neg} (e), \ProdsndMACRoAA {x_{3}}))}$.

Finset.mulDysonETransformdefMathlib.Combinatorics.Additive.ETransform, function or constant

Wording

no wording

English

Let $e$ be an element of $x$. Let $x_{3}$ be an element of $\mathrm{Prod}$ applied to the set of finite sets of $x$ and the set of finite sets of $x$. Then $\operatorname{mulDysonETransform}$ applied to $e$ and $x_{3}$ is an element of $\mathrm{Prod}$ applied to the set of finite sets of $x$ and the set of finite sets of $x$ defined as $\ProdmkMACRoU {(\UnionunionMACRoAB {\ProdfstMACRoZ {x_{3}}}{(\HSMulhSMulMACRoAL {e}{\ProdsndMACRoAA {x_{3}}})})}{\operatorname{inter} (\ProdsndMACRoAA {x_{3}}, \HSMulhSMulMACRoAL {\operatorname{inv} (e)}{\ProdfstMACRoZ {x_{3}}})}$.

Finset.mulETransformLeftdefMathlib.Combinatorics.Additive.ETransform, function or constant

Wording

the left multiplicative transform of e and x3 (from the name)

English

Let $e$ be an element of $x$. Let $x_{3}$ be an element of $\mathrm{Prod}$ applied to the set of finite sets of $x$ and the set of finite sets of $x$. Then the left multiplicative transform of $e$ and $x_{3}$ is an element of $\mathrm{Prod}$ applied to the set of finite sets of $x$ and the set of finite sets of $x$ defined as $\ProdmkMACRoU {\operatorname{inter} (\ProdfstMACRoZ {x_{3}}, \HSMulhSMulMACRoAL {\operatorname{op} (e)}{\ProdfstMACRoZ {x_{3}}})}{(\UnionunionMACRoAB {\ProdsndMACRoAA {x_{3}}}{(\HSMulhSMulMACRoAL {\operatorname{inv} (e)}{\ProdsndMACRoAA {x_{3}}})})}$.

Finset.mulETransformRightdefMathlib.Combinatorics.Additive.ETransform, function or constant

Wording

the right multiplicative transform of e and x3 (from the name)

English

Let $e$ be an element of $x$. Let $x_{3}$ be an element of $\mathrm{Prod}$ applied to the set of finite sets of $x$ and the set of finite sets of $x$. Then the right multiplicative transform of $e$ and $x_{3}$ is an element of $\mathrm{Prod}$ applied to the set of finite sets of $x$ and the set of finite sets of $x$ defined as $\ProdmkMACRoU {(\UnionunionMACRoAB {\ProdfstMACRoZ {x_{3}}}{(\HSMulhSMulMACRoAL {\operatorname{op} (e)}{\ProdfstMACRoZ {x_{3}}})})}{\operatorname{inter} (\ProdsndMACRoAA {x_{3}}, \HSMulhSMulMACRoAL {\operatorname{inv} (e)}{\ProdsndMACRoAA {x_{3}}})}$.

Mathlib.Combinatorics.Additive.Energy

Finset.addEnergydefMathlib.Combinatorics.Additive.Energy, function or constant

Wording

the additive energy of s and t (from the docstring)

English

Let $s$ and $t$ be finite sets of $x$. Then the additive energy of $s$ and $t$ is a natural number defined as the cardinality of $\FinsetFilter {x_{3}}{(\EqtMACRoH {(\ProdfstMACRoZ {\ProdfstMACRoZ {x_{3}}}+ \ProdfstMACRoZ {\ProdsndMACRoAA {x_{3}}})}{(\ProdsndMACRoAA {\ProdfstMACRoZ {x_{3}}}+ \ProdsndMACRoAA {\ProdsndMACRoAA {x_{3}}})})}{\operatorname{sprod} (\operatorname{sprod} (s , s), \operatorname{sprod} (t , t))}$.

Finset.mulEnergydefMathlib.Combinatorics.Additive.Energy, function or constant

Wording

the multiplicative energy of s and t (from the docstring)

English

Let $s$ and $t$ be finite sets of $x$. Then the multiplicative energy of $s$ and $t$ is a natural number defined as the cardinality of $\FinsetFilter {x_{3}}{(\EqtMACRoH {(\ProdfstMACRoZ {\ProdfstMACRoZ {x_{3}}}\times \ProdfstMACRoZ {\ProdsndMACRoAA {x_{3}}})}{(\ProdsndMACRoAA {\ProdfstMACRoZ {x_{3}}}\times \ProdsndMACRoAA {\ProdsndMACRoAA {x_{3}}})})}{\operatorname{sprod} (\operatorname{sprod} (s , s), \operatorname{sprod} (t , t))}$.

Mathlib.Combinatorics.Additive.FreimanHom

IsAddFreimanHomstructureMathlib.Combinatorics.Additive.FreimanHom, predicate

Wording

no wording

English

Let $n$ be a natural number. Let $A$ be an element of $\wp x$. Let $B$ be an element of $\wp x_{1}$. Let $f$ be a function from elements of $x$ to elements of $x_{1}$. Then we can say that $\mathrm{IsAddFreimanHom}$ holds for $n$, $A$, $B$ and $f$.

IsAddFreimanIsostructureMathlib.Combinatorics.Additive.FreimanHom, predicate

Wording

no wording

English

IsMulFreimanHomstructureMathlib.Combinatorics.Additive.FreimanHom, predicate

Wording

no wording

English

IsMulFreimanIsostructureMathlib.Combinatorics.Additive.FreimanHom, predicate

Wording

no wording

English

Mathlib.Combinatorics.Additive.SubsetSum

Finset.subsetSumdefMathlib.Combinatorics.Additive.SubsetSum, function or constant

Wording

the subset sum of A (from the name)

English

Let $A$ be a finite set of $M$. Then the subset sum of $A$ is a finite set of $M$ defined as the forward image of the powerset of $A$ under the function that maps $B$ to $\FinsetSum {B}{a}{\mathrm{id} (a)}$.

Mathlib.Combinatorics.Additive.VerySmallDoubling

Finset.invMulSubgroupdefMathlib.Combinatorics.Additive.VerySmallDoubling, function or constant

Wording

the inverse multiplicative subgroup of A and h (from the name)

English

Let $A$ be a finite set of $G$ such that $\FinsetcardMACRoM {(A \times A)}< \frac{ 3}{2}\times \FinsetcardMACRoM {A}$. Then the inverse multiplicative subgroup of $A$ and $h$ is a subgroup of $G$.

Mathlib.Combinatorics.Colex

Finset.Colex.IsInitSegdefMathlib.Combinatorics.Colex, predicate

Wording

no wording

English

Let $x_{2}$ be a finite set of the set of finite sets of $x$. Let $r$ be a natural number. Then $\operatorname{IsInitSeg}$ holds for $x_{2}$ and $r$, if $\operatorname{Sized}$ holds for $r$ and $x_{2}$ and for all finite sets $s$ of $x$, for all finite sets $t$ of $x$, if $s$ is an element of $x_{2}$, then if $\operatorname{toColex} (t)< \operatorname{toColex} (s)$ and $\FinsetcardMACRoM {t}= r$, then $t$ is an element of $x_{2}$.

Finset.Colex.initSegdefMathlib.Combinatorics.Colex, function or constant

Wording

no wording

English

Let $s$ be a finite set of $x$. Then $\operatorname{initSeg}$ applied to $s$ is a finite set of the set of finite sets of $x$ defined as $\FinsetFilter {t}{\mathrm{and} (\mathrm{Eq} (\FinsetcardMACRoM {s}, \FinsetcardMACRoM {t}), \mathrm{Leq} (\operatorname{toColex} (t), \operatorname{toColex} (s)))}{\FinsetunivMACRoAC}$.

Finset.equivBitIndicesdefMathlib.Combinatorics.Colex, function or constant

Wording

the equivalence bit indice (from the name)

English

The equivalence bit indice is an equivalence from $\Natural$ to the set of finite sets of $\Natural$ defined as $\operatorname{mk}$ applied to the function that maps $n$ to the finite set of the bit indice of $n$, the function that maps $s$ to $\FinsetSum {s}{i}{(2 ^ {i})}$, $\mathrm{Finset\_\_sum\_toFinset\_bitIndices\_two\_pow}$ and $\mathrm{Finset\_\_toFinset\_bitIndices\_sum\_two\_pow}$.

Finset.orderIsoColexdefMathlib.Combinatorics.Colex, function or constant

Wording

no wording

English

$\operatorname{orderIsoColex}$ is an order isomorphism of $\Natural$ and $\mathrm{Colex}$ applied to the set of finite sets of $\Natural$.

Mathlib.Combinatorics.Configuration

Configuration.DualdefMathlib.Combinatorics.Configuration, type

Wording

dual of P (from the name)

English

Let $P$ be a set. Then a dual of $P$ is an element of the function that maps $P$ to $P$.

Configuration.HasLinesclassMathlib.Combinatorics.Configuration, predicate

Wording

no wording

English

Let $P$ and $L$ be sets. Then we can say that $\operatorname{HasLines}$ holds for $P$ and $L$.

Configuration.HasLines.mkLinedefMathlib.Combinatorics.Configuration, function or constant

Wording

the line of h (from the name)

English

Assume that $x_{1} \neq x_{2}$. Then the line of $h$ is an element of $L$ defined as $\operatorname{proj1}$ applied to $\mathrm{self}$ and $h$.

Configuration.HasPointsclassMathlib.Combinatorics.Configuration, predicate

Wording

no wording

English

Let $P$ and $L$ be sets. Then we can say that $\operatorname{HasPoints}$ holds for $P$ and $L$.

Configuration.HasPoints.mkPointdefMathlib.Combinatorics.Configuration, function or constant

Wording

the point of h (from the name)

English

Assume that $x_{1} \neq x_{2}$. Then the point of $h$ is an element of $P$ defined as $\operatorname{proj1}$ applied to $\mathrm{self}$ and $h$.

Configuration.NondegenerateclassMathlib.Combinatorics.Configuration, predicate

Wording

no wording

English

Let $P$ and $L$ be sets. Then we can say that $\operatorname{Nondegenerate}$ holds for $P$ and $L$.

Configuration.ProjectivePlaneclassMathlib.Combinatorics.Configuration, predicate

Wording

no wording

English

Let $P$ and $L$ be sets. Then we can say that $\operatorname{ProjectivePlane}$ holds for $P$ and $L$.

Configuration.ProjectivePlane.mkLinedefMathlib.Combinatorics.Configuration, function or constant

Wording

the line of h (from the name)

English

Assume that $x_{1} \neq x_{2}$. Then the line of $h$ is an element of $L$ defined as $\operatorname{proj1}$ applied to $\mathrm{self}$ and $h$.

Configuration.ProjectivePlane.orderdefMathlib.Combinatorics.Configuration, function or constant

Wording

the order of P and L (from the docstring)

English

Let $P$ and $L$ be sets. Then the order of $P$ and $L$ is a natural number defined as the difference between the line count of $L$ and $\operatorname{choose}$ applied to $\mathrm{Configuration\_\_ProjectivePlane\_\_exists\_config}$ and $1$.

Configuration.lineCountdefMathlib.Combinatorics.Configuration, function or constant

Wording

the line count of L and p (from the name)

English

Let $L$ be a set. Let $p$ be an element of $P$. Then the line count of $L$ and $p$ is a natural number defined as the cardinality of $\SubtypeSet {l}{(\MembershipmemMACRoT {l}{p})}$.

Configuration.pointCountdefMathlib.Combinatorics.Configuration, function or constant

Wording

the point count of P and l (from the name)

English

Let $P$ be a set. Let $l$ be an element of $L$. Then the point count of $P$ and $l$ is a natural number defined as the cardinality of $\SubtypeSet {p}{(\MembershipmemMACRoT {l}{p})}$.

Mathlib.Combinatorics.Derangements.Basic

Equiv.derangementsCongrdefMathlib.Combinatorics.Derangements.Basic, function or constant

Wording

the derangement congruence of e (from the name)

English

Let $e$ be an equivalence from $x$ to $x_{1}$. Then the derangement congruence of $e$ is an equivalence from the set of elements of the derangement of $x$ to the set of elements of the derangement of $x_{1}$.

derangementsdefMathlib.Combinatorics.Derangements.Basic, function or constant

Wording

the derangement of x (from the name)

English

Let $x$ be a set. Then the derangement of $x$ is an element of the power set of the set of permutations of $x$ defined as $\operatorname{ofPred}$ applied to the function that maps $f$ to the proposition that for all elements $x_{1}$ of $x$, $f (x_{1})\neq x_{1}$.

derangements.Equiv.RemoveNone.fiberdefMathlib.Combinatorics.Derangements.Basic, function or constant

Wording

the fiber of a (from the name)

English

Let $a$ be an element of $\mathrm{Option}$ applied to $x$. Then the fiber of $a$ is an element of the power set of the set of permutations of $x$ defined as $\operatorname{ofPred}$ applied to the function that maps $f$ to the proposition that $\ProdmkMACRoU {a}{f}$ is an element of the image of $\operatorname{coe}$ applied to $\operatorname{decomposeOption}$ and the derangement of $\mathrm{Option}$ applied to $x$.

derangements.atMostOneFixedPointEquivSum_derangementsdefMathlib.Combinatorics.Derangements.Basic, function or constant

Wording

no wording

English

Let $a$ be an element of $x$. Then $\mathrm{derangements\_\_atMostOneFixedPointEquivSum\_derangements}$ applied to $a$ is an element of $\EquivMACRoAE {(\SubtypeSet {f}{\mathrm{Leq} (\operatorname{fixedPoints} (\operatorname{coe} (f)), \operatorname{singleton} (a))})}{\mathrm{Sum} (\operatorname{Elem} (\mathrm{derangements} (\operatorname{Elem} (\operatorname{compl} (\operatorname{singleton} (a))))), \operatorname{Elem} (\mathrm{derangements} (x)))}$.

derangements.derangementsOptionEquivSigmaAtMostOneFixedPointdefMathlib.Combinatorics.Derangements.Basic, function or constant

Wording

the derangement option equivalence sigma at most one fixed point (from the name)

English

The derangement option equivalence sigma at most one fixed point is an equivalence from the set of elements of the derangement of $\mathrm{Option}$ applied to $x$ to $\Sigma$ applied to the function that maps $a$ to the set of elements of $\operatorname{ofPred}$ applied to the function that maps $f$ to the proposition that the fixed point of $\operatorname{coe}$ applied to $f$ is less than or equal to $\operatorname{singleton}$ applied to $a$.

derangements.derangementsRecursionEquivdefMathlib.Combinatorics.Derangements.Basic, function or constant

Wording

the derangement recursion equivalence (from the name)

English

The derangement recursion equivalence is an equivalence from the set of elements of the derangement of $\mathrm{Option}$ applied to $x$ to $\Sigma$ applied to the function that maps $a$ to $\mathrm{Sum}$ applied to the set of elements of the derangement of the set of elements of the complement of $\operatorname{singleton}$ applied to $a$ and the set of elements of the derangement of $x$ defined as the composition of the derangement option equivalence sigma at most one fixed point and the right sigma congruence of $\mathrm{derangements\_\_atMostOneFixedPointEquivSum\_derangements}$.

derangements.subtypeEquivdefMathlib.Combinatorics.Derangements.Basic, function or constant

Wording

the subtype equivalence of p (from the name)

English

Let $p$ be a function from elements of $x$ to propositions. Then the subtype equivalence of $p$ is an element of $\EquivMACRoAE {\operatorname{Elem} (\mathrm{derangements} (\SubtypeSet {x_{2}}{p (x_{2})}))}{(\SubtypeSet {f}{\mathrm{forall} (x , \lambda a . \mathrm{iff} (\mathrm{not} (p (a)), \MembershipmemMACRoT {\operatorname{fixedPoints} (\operatorname{coe} (f))}{a}))})}$.

Mathlib.Combinatorics.Derangements.Finite

numDerangementsdefMathlib.Combinatorics.Derangements.Finite, function or constant

Wording

the numerator derangement of x (from the name)

English

Let $x$ be a natural number. Then the numerator derangement of $x$ is a natural number defined as $\operatorname{brecOn}$ applied to $x$ and $\mathrm{numDerangements\_\_\_f}$.

Mathlib.Combinatorics.Digraph.Basic

DigraphstructureMathlib.Combinatorics.Digraph.Basic, type

Wording

digraph of V (from the name)

English

Let $V$ be a set. Then the digraphs of $V$ are a basic type.

Digraph.AdjdefMathlib.Combinatorics.Digraph.Basic, predicate

Wording

no wording

English

Let $\mathrm{self}$ be a digraph of $V$. Let $x$ and $x_{1}$ be elements of $V$. Then $\operatorname{Adj}$ holds for $\mathrm{self}$, $x$ and $x_{1}$, if $\operatorname{proj0}$ holds for $\mathrm{self}$, $x$ and $x_{1}$.

Digraph.IsSubgraphdefMathlib.Combinatorics.Digraph.Basic, predicate

Wording

no wording

English

Let $x$ and $y$ be digraphs of $V$. Then $\operatorname{IsSubgraph}$ holds for $x$ and $y$, if for all elements $v$ and $w$ of $V$, if $\operatorname{Adj}$ holds for $x$, $v$ and $w$, then $\operatorname{Adj}$ holds for $y$, $v$ and $w$.

Digraph.completeBipartiteGraphdefMathlib.Combinatorics.Digraph.Basic, function or constant

Wording

the complete bipartite graph of V and W (from the name)

English

Let $V$ and $W$ be sets. Then the complete bipartite graph of $V$ and $W$ is a digraph of $\mathrm{Sum}$ applied to $V$ and $W$ defined as $\operatorname{mk}$ applied to the function that maps $v$ and $w$ to the proposition that $\EqtMACRoH {\operatorname{isLeft} (v)}{\operatorname{true}}$ and $\EqtMACRoH {\operatorname{isRight} (w)}{\operatorname{true}}$ or $\EqtMACRoH {\operatorname{isRight} (v)}{\operatorname{true}}$ and $\EqtMACRoH {\operatorname{isLeft} (w)}{\operatorname{true}}$.

Digraph.completeDigraphdefMathlib.Combinatorics.Digraph.Basic, function or constant

Wording

the complete digraph of V (from the name)

English

Let $V$ be a set. Then the complete digraph of $V$ is a digraph of $V$ defined as $\operatorname{mk}$ applied to the top.

Digraph.emptyDigraphdefMathlib.Combinatorics.Digraph.Basic, function or constant

Wording

the empty digraph of V (from the name)

English

Let $V$ be a set. Then the empty digraph of $V$ is a digraph of $V$ defined as $\operatorname{mk}$ applied to the function that maps $x$ and $x_{1}$ to the proposition that we have a contradiction.

Digraph.mk'defMathlib.Combinatorics.Digraph.Basic, function or constant

Wording

no wording

English

$\operatorname{mk'}$ is an embedding of the set of functions from elements of $V$ and elements of $V$ to elements of $\mathrm{Bool}$ and the set of digraphs of $V$.

Mathlib.Combinatorics.Digraph.Orientation

Digraph.toSimpleGraphInclusivedefMathlib.Combinatorics.Digraph.Orientation, function or constant

Wording

no wording

English

Let $G$ be a digraph of $V$. Then $\operatorname{toSimpleGraphInclusive}$ applied to $G$ is a simple graph of $V$ defined as $\operatorname{fromRel}$ applied to $\operatorname{Adj}$ applied to $G$.

Digraph.toSimpleGraphStrictdefMathlib.Combinatorics.Digraph.Orientation, function or constant

Wording

no wording

English

Let $G$ be a digraph of $V$. Then $\operatorname{toSimpleGraphStrict}$ applied to $G$ is a simple graph of $V$.

Mathlib.Combinatorics.Enumerative.Bell

Multiset.belldefMathlib.Combinatorics.Enumerative.Bell, function or constant

Wording

no wording

English

Let $m$ be a multiset of $\Natural$. Then $\operatorname{bell}$ applied to $m$ is an element of $\Natural$ defined as $\operatorname{multinomial} (\operatorname{toFinset} (m), \lambda k . k \times \operatorname{count} (k , m))\times \FinsetProd {\operatorname{erase} (\operatorname{toFinset} (m), 0)}{k_{1}}{(\FinsetProd {\FinsetrangeMACRoN {\operatorname{count} (k_{1} , m)}}{j}{\operatorname{choose} (j \times k_{1} + k_{1} - 1 , k_{1} - 1)})}$.

Nat.belldefMathlib.Combinatorics.Enumerative.Bell, function or constant

Wording

no wording

English

Let $x$ be a natural number. Then $\operatorname{bell}$ applied to $x$ is a natural number.

Nat.uniformBelldefMathlib.Combinatorics.Enumerative.Bell, function or constant

Wording

no wording

English

Let $m$ and $n$ be natural numbers. Then $\operatorname{uniformBell}$ applied to $m$ and $n$ is a natural number defined as $\operatorname{bell}$ applied to $\operatorname{replicate}$ applied to $m$ and $n$.

Mathlib.Combinatorics.Enumerative.Catalan.Basic

catalandefMathlib.Combinatorics.Enumerative.Catalan.Basic, function or constant

Wording

no wording

English

Let $x$ be a natural number. Then $\mathrm{catalan}$ applied to $x$ is a natural number.

Mathlib.Combinatorics.Enumerative.Catalan.Tree

BinaryTree.pairwiseNodedefMathlib.Combinatorics.Enumerative.Catalan.Tree, function or constant

Wording

the pairwise node of a and b (from the name)

English

Let $a$ and $b$ be finite sets of the set of binary trees of $\mathrm{Unit}$. Then the pairwise node of $a$ and $b$ is a finite set of the set of binary trees of $\mathrm{Unit}$.

BinaryTree.treesOfNumNodesEqdefMathlib.Combinatorics.Enumerative.Catalan.Tree, function or constant

Wording

the tree of x (from the name)

English

Let $x$ be a natural number. Then the tree of $x$ is a finite set of the set of binary trees of $\mathrm{Unit}$.

Mathlib.Combinatorics.Enumerative.Composition

CompositionstructureMathlib.Combinatorics.Enumerative.Composition, type

Wording

composition of n (from the name)

English

Let $n$ be a natural number. Then the compositions of $n$ are a basic type.

Composition.appenddefMathlib.Combinatorics.Enumerative.Composition, function or constant

Wording

no wording

English

Let $x$ be a composition of $m$. Let $x_{1}$ be a composition of $n$. Then $\operatorname{append}$ applied to $x$ and $x_{1}$ is a composition of $m + n$.

Composition.blocksdefMathlib.Combinatorics.Enumerative.Composition, function or constant

Wording

the block of self (from the name)

English

Let $\mathrm{self}$ be a composition of $n$. Then the block of $\mathrm{self}$ is a list of natural numbers defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.

Composition.blocksFinEquivdefMathlib.Combinatorics.Enumerative.Composition, function or constant

Wording

the block finite equivalence of c (from the name)

English

Let $c$ be a composition of $n$. Then the block finite equivalence of $c$ is an equivalence from $\Sigma$ applied to the function that maps $i$ to $\mathrm{Fin}$ applied to the block function of $c$ and $i$ to $\mathrm{Fin}$ applied to $n$.

Composition.blocksFundefMathlib.Combinatorics.Enumerative.Composition, function or constant

Wording

the block function of c and x (from the name)

English

Let $c$ be a composition of $n$. Let $x$ be an element of $\mathrm{Fin}$ applied to the length of $c$. Then the block function of $c$ and $x$ is a natural number defined as $\operatorname{get}$ applied to the block of $c$ and $x$.

Composition.boundariesdefMathlib.Combinatorics.Enumerative.Composition, function or constant

Wording

the boundary of c (from the name)

English

Let $c$ be a composition of $n$. Then the boundary of $c$ is a finite set of $\mathrm{Fin}$ applied to $n + 1$ defined as the map of $\operatorname{toEmbedding}$ applied to the boundary of $c$ and the universal set.

Composition.boundarydefMathlib.Combinatorics.Enumerative.Composition, function or constant

Wording

the boundary of c (from the name)

English

Let $c$ be a composition of $n$. Then the boundary of $c$ is an order embedding of $\mathrm{Fin}$ applied to the sum of the length of $c$ and $1$ and $\mathrm{Fin}$ applied to $n + 1$.

Composition.castdefMathlib.Combinatorics.Enumerative.Composition, function or constant

Wording

the cast of c and hmn (from the name)

English

Let $c$ be a composition of $m$. Assume that $m = n$. Then the cast of $c$ and $\mathrm{hmn}$ is a composition of $n$.

Composition.embeddingdefMathlib.Combinatorics.Enumerative.Composition, function or constant

Wording

the embedding of c and i (from the name)

English

Let $c$ be a composition of $n$. Let $i$ be an element of $\mathrm{Fin}$ applied to the length of $c$. Then the embedding of $c$ and $i$ is an order embedding of $\mathrm{Fin}$ applied to the block function of $c$ and $i$ and $\mathrm{Fin}$ applied to $n$.

Composition.indexdefMathlib.Combinatorics.Enumerative.Composition, function or constant

Wording

the index of c and j (from the name)

English

Let $c$ be a composition of $n$. Let $j$ be an element of $\mathrm{Fin}$ applied to $n$. Then the index of $c$ and $j$ is an element of $\mathrm{Fin}$ applied to the length of $c$.

Composition.invEmbeddingdefMathlib.Combinatorics.Enumerative.Composition, function or constant

Wording

the inverse embedding of c and j (from the name)

English

Let $c$ be a composition of $n$. Let $j$ be an element of $\mathrm{Fin}$ applied to $n$. Then the inverse embedding of $c$ and $j$ is an element of $\mathrm{Fin}$ applied to the block function of $c$ and the index of $c$ and $j$.

Composition.lengthdefMathlib.Combinatorics.Enumerative.Composition, function or constant

Wording

the length of c (from the docstring)

English

Let $c$ be a composition of $n$. Then the length of $c$ is a natural number defined as $\operatorname{length}$ applied to the block of $c$.

Composition.onesdefMathlib.Combinatorics.Enumerative.Composition, function or constant

Wording

the one of n (from the name)

English

Let $n$ be a natural number. Then the one of $n$ is a composition of $n$.

Composition.recOnAppendSingledefMathlib.Combinatorics.Enumerative.Composition, function or constant

Wording

no wording

English

Let $c$ be a composition of $n$. Let $\mathrm{zero}$ be an element of $\mathrm{motive}$ applied to $0$ and the one of $0$. Let $\mathrm{append\_single}$ be a function from natural numbers $k$ and natural numbers $n_{1}$ and compositions $c_{1}$ of $n_{1}$ and elements of $\mathrm{motive}$ applied to $n_{1}$ and $c_{1}$ to elements of $\mathrm{motive}$ applied to $n_{1} + (k + 1)$ and $\operatorname{append}$ applied to $c_{1}$ and $\operatorname{single}$ applied to $k + 1$ and $\mathrm{Nat\_\_succ\_pos}$ applied to $k$. Then $\operatorname{recOnAppendSingle}$ applied to $c$, $\mathrm{zero}$, $k$, $n_{1}$, $c_{1}$ and $\mathrm{append\_single}$ is an element of $\mathrm{motive}$ applied to $n$ and $c$.

Composition.recOnSingleAppenddefMathlib.Combinatorics.Enumerative.Composition, function or constant

Wording

no wording

English

Let $c$ be a composition of $n$. Let $\mathrm{zero}$ be an element of $\mathrm{motive}$ applied to $0$ and the one of $0$. Let $\mathrm{single\_append}$ be a function from natural numbers $k$ and natural numbers $n_{1}$ and compositions $c_{1}$ of $n_{1}$ and elements of $\mathrm{motive}$ applied to $n_{1}$ and $c_{1}$ to elements of $\mathrm{motive}$ applied to $k + 1 + n_{1}$ and $\operatorname{append}$ applied to $\operatorname{single}$ applied to $k + 1$ and $\mathrm{Nat\_\_succ\_pos}$ applied to $k$ and $c_{1}$. Then $\operatorname{recOnSingleAppend}$ applied to $c$, $\mathrm{zero}$, $k$, $n_{1}$, $c_{1}$ and $\mathrm{single\_append}$ is an element of $\mathrm{motive}$ applied to $n$ and $c$ defined as the function that maps $n_{1}$, $c_{1}$ and $\mathrm{single\_append}$ to $\mathrm{Composition\_\_recOnSingleAppend\_\_\_unary}$ applied to $\mathrm{zero}$, $k$, $\operatorname{mk}$ applied to $n$ and $c$, $n_{1}$, $c_{1}$ and $\mathrm{single\_append}$.

Composition.reversedefMathlib.Combinatorics.Enumerative.Composition, function or constant

Wording

the reverse of c (from the name)

English

Let $c$ be a composition of $n$. Then the reverse of $c$ is a composition of $n$.

Composition.singledefMathlib.Combinatorics.Enumerative.Composition, function or constant

Wording

no wording

English

Let $n$ be a natural number such that $0 < n$. Then $\operatorname{single}$ applied to $n$ and $h$ is a composition of $n$.

Composition.sizeUpTodefMathlib.Combinatorics.Enumerative.Composition, function or constant

Wording

no wording

English

Let $c$ be a composition of $n$. Let $i$ be a natural number. Then $\operatorname{sizeUpTo}$ applied to $c$ and $i$ is a natural number defined as $\operatorname{sum}$ applied to $\operatorname{take}$ applied to $i$ and the block of $c$.

Composition.toCompositionAsSetdefMathlib.Combinatorics.Enumerative.Composition, function or constant

Wording

the composition as set of c (from the name)

English

Let $c$ be a composition of $n$. Then the composition as set of $c$ is a composition as set of $n$.

CompositionAsSetstructureMathlib.Combinatorics.Enumerative.Composition, type

Wording

composition as set of n (from the name)

English

Let $n$ be a natural number. Then the compositions as set of $n$ are a basic type.

CompositionAsSet.blocksdefMathlib.Combinatorics.Enumerative.Composition, function or constant

Wording

the block of c (from the name)

English

Let $c$ be a composition as set of $n$. Then the block of $c$ is a list of natural numbers defined as $\operatorname{ofFn}$ applied to $\operatorname{blocksFun}$ applied to $c$.

CompositionAsSet.blocksFundefMathlib.Combinatorics.Enumerative.Composition, function or constant

Wording

the block function of c and i (from the name)

English

Let $c$ be a composition as set of $n$. Let $i$ be an element of $\mathrm{Fin}$ applied to the length of $c$. Then the block function of $c$ and $i$ is a natural number defined as $\operatorname{val} (\operatorname{boundary} (c , \operatorname{mk} (\operatorname{val} (i)+ 1 , \mathrm{CompositionAsSet\_\_lt\_length} (c , i))))- \operatorname{val} (\operatorname{boundary} (c , \operatorname{mk} (\operatorname{val} (i), \mathrm{CompositionAsSet\_\_lt\_length'} (c , i))))$.

CompositionAsSet.boundariesdefMathlib.Combinatorics.Enumerative.Composition, function or constant

Wording

the boundary of self (from the name)

English

Let $\mathrm{self}$ be a composition as set of $n$. Then the boundary of $\mathrm{self}$ is a finite set of $\mathrm{Fin}$ applied to the successor of $n$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.

CompositionAsSet.boundarydefMathlib.Combinatorics.Enumerative.Composition, function or constant

Wording

the boundary of c (from the name)

English

Let $c$ be a composition as set of $n$. Then the boundary of $c$ is an order embedding of $\mathrm{Fin}$ applied to the cardinality of the boundary of $c$ and $\mathrm{Fin}$ applied to $n + 1$.

CompositionAsSet.lengthdefMathlib.Combinatorics.Enumerative.Composition, function or constant

Wording

the length of c (from the name)

English

Let $c$ be a composition as set of $n$. Then the length of $c$ is a natural number defined as the difference between the cardinality of the boundary of $c$ and $1$.

CompositionAsSet.toCompositiondefMathlib.Combinatorics.Enumerative.Composition, function or constant

Wording

the composition of c (from the name)

English

Let $c$ be a composition as set of $n$. Then the composition of $c$ is a composition of $n$.

List.splitWrtCompositiondefMathlib.Combinatorics.Enumerative.Composition, function or constant

Wording

no wording

English

Let $l$ be a list of elements of $x$. Let $c$ be a composition of $n$. Then $\operatorname{splitWrtComposition}$ applied to $l$ and $c$ is a list of lists of elements of $x$ defined as $\operatorname{splitWrtCompositionAux}$ applied to $l$ and the block of $c$.

compositionAsSetEquivdefMathlib.Combinatorics.Enumerative.Composition, function or constant

Wording

the composition as set equivalence of n (from the name)

English

Let $n$ be a natural number. Then the composition as set equivalence of $n$ is an equivalence from the set of compositions as set of $n$ to the set of finite sets of $\mathrm{Fin}$ applied to $n - 1$.

compositionEquivdefMathlib.Combinatorics.Enumerative.Composition, function or constant

Wording

the composition equivalence of n (from the name)

English

Let $n$ be a natural number. Then the composition equivalence of $n$ is an equivalence from the set of compositions of $n$ to the set of compositions as set of $n$.

Mathlib.Combinatorics.Enumerative.DoubleCounting

Finset.bipartiteAbovedefMathlib.Combinatorics.Enumerative.DoubleCounting, function or constant

Wording

no wording

English

Let $r$ be a function from elements of $x$ and elements of $x_{1}$ to propositions. Let $t$ be a finite set of $x_{1}$. Let $a$ be an element of $x$. Then $\operatorname{bipartiteAbove}$ applied to $r$, $t$ and $a$ is a finite set of $x_{1}$ defined as $\FinsetFilter {b}{r (a , b)}{t}$.

Finset.bipartiteBelowdefMathlib.Combinatorics.Enumerative.DoubleCounting, function or constant

Wording

no wording

English

Let $r$ be a function from elements of $x$ and elements of $x_{1}$ to propositions. Let $s$ be a finite set of $x$. Let $b$ be an element of $x_{1}$. Then $\operatorname{bipartiteBelow}$ applied to $r$, $s$ and $b$ is a finite set of $x$ defined as $\FinsetFilter {a}{r (a , b)}{s}$.

Mathlib.Combinatorics.Enumerative.DyckWord

DyckStepinductiveMathlib.Combinatorics.Enumerative.DyckWord, type

Wording

no wording

English

The elements of $\mathrm{DyckStep}$ are a basic type.

DyckStep.DconstructorMathlib.Combinatorics.Enumerative.DyckWord, function or constant

Wording

no wording

English

$\operatorname{D}$ is an element of $\mathrm{DyckStep}$.

DyckStep.UconstructorMathlib.Combinatorics.Enumerative.DyckWord, function or constant

Wording

no wording

English

$\operatorname{U}$ is an element of $\mathrm{DyckStep}$.

DyckStep.ctorElimTypedefMathlib.Combinatorics.Enumerative.DyckWord, type

Wording

no wording

English

DyckStep.ofNatdefMathlib.Combinatorics.Enumerative.DyckWord, function or constant

Wording

no wording

English

Let $x$ be a natural number. Then $\operatorname{ofNat}$ applied to $x$ is an element of $\mathrm{DyckStep}$ defined as $\mathrm{cond}$ applied to $\operatorname{ble}$ applied to $x$ and $0$, $\operatorname{U}$ and $\operatorname{D}$.

DyckWordstructureMathlib.Combinatorics.Enumerative.DyckWord, type

Wording

no wording

English

The elements of $\mathrm{DyckWord}$ are a basic type.

DyckWord.IsNesteddefMathlib.Combinatorics.Enumerative.DyckWord, predicate

Wording

p is nested (from the name)

English

Let $p$ be an element of $\mathrm{DyckWord}$. Then $p$ is nested, if $p \neq 0$ and for all natural numbers $i$, if $0 < i$, then if $i$ is less than $\operatorname{length}$ applied to the underlying list of $p$, then the multiplicity of $\operatorname{D}$ in $\operatorname{take}$ applied to $i$ and the underlying list of $p$ is less than the multiplicity of $\operatorname{U}$ in $\operatorname{take}$ applied to $i$ and the underlying list of $p$.

DyckWord.denestdefMathlib.Combinatorics.Enumerative.DyckWord, function or constant

Wording

no wording

English

Let $p$ be a nested element of $\mathrm{DyckWord}$. Then $\operatorname{denest}$ applied to $p$ and $\mathrm{hn}$ is an element of $\mathrm{DyckWord}$.

DyckWord.dropdefMathlib.Combinatorics.Enumerative.DyckWord, function or constant

Wording

no wording

English

Let $p$ be an element of $\mathrm{DyckWord}$. Let $i$ be a natural number such that the multiplicity of $\operatorname{U}$ in $\operatorname{take}$ applied to $i$ and the underlying list of $p$ is equal to the multiplicity of $\operatorname{D}$ in $\operatorname{take}$ applied to $i$ and the underlying list of $p$. Then $\operatorname{drop}$ applied to $p$, $i$ and $\mathrm{hi}$ is an element of $\mathrm{DyckWord}$.

DyckWord.equivTreedefMathlib.Combinatorics.Enumerative.DyckWord, function or constant

Wording

the equivalence tree (from the name)

English

The equivalence tree is an equivalence from $\mathrm{DyckWord}$ to the set of binary trees of $\mathrm{Unit}$ defined as $\operatorname{mk}$ applied to $\operatorname{toTree}$, $\operatorname{ofTree}$, $\mathrm{DyckWord\_\_ofTree\_toTree}$ and $\mathrm{DyckWord\_\_toTree\_ofTree}$.

DyckWord.equivTreesOfNumNodesEqdefMathlib.Combinatorics.Enumerative.DyckWord, function or constant

Wording

the equivalence tree of n (from the name)

English

Let $n$ be an element of $\Natural$. Then the equivalence tree of $n$ is an element of $\EquivMACRoAE {(\SubtypeSet {p}{\mathrm{Eq} (\operatorname{semilength} (p), n)})}{(\SubtypeSet {x}{(\MembershipmemMACRoT {\operatorname{treesOfNumNodesEq} (n)}{x})})}$.

DyckWord.firstReturndefMathlib.Combinatorics.Enumerative.DyckWord, function or constant

Wording

no wording

English

Let $p$ be an element of $\mathrm{DyckWord}$. Then $\operatorname{firstReturn}$ applied to $p$ is a natural number defined as $\operatorname{findIdx}$ applied to the function that maps $i$ to $\operatorname{decide}$ applied to the proposition that the multiplicity of $\operatorname{U}$ in $\operatorname{take}$ applied to $i + 1$ and the underlying list of $p$ is equal to the multiplicity of $\operatorname{D}$ in $\operatorname{take}$ applied to $i + 1$ and the underlying list of $p$ and $\operatorname{range}$ applied to $\operatorname{length}$ applied to the underlying list of $p$.

DyckWord.insidePartdefMathlib.Combinatorics.Enumerative.DyckWord, function or constant

Wording

no wording

English

Let $p$ be an element of $\mathrm{DyckWord}$. Then $\operatorname{insidePart}$ applied to $p$ is an element of $\mathrm{DyckWord}$.

DyckWord.nestdefMathlib.Combinatorics.Enumerative.DyckWord, function or constant

Wording

no wording

English

Let $p$ be an element of $\mathrm{DyckWord}$. Then $\operatorname{nest}$ applied to $p$ is an element of $\mathrm{DyckWord}$.

DyckWord.ofTreedefMathlib.Combinatorics.Enumerative.DyckWord, function or constant

Wording

no wording

English

Let $x$ be a binary tree of $\mathrm{Unit}$. Then $\operatorname{ofTree}$ applied to $x$ is an element of $\mathrm{DyckWord}$ defined as $\operatorname{brecOn}$ applied to $x$ and $\mathrm{DyckWord\_\_ofTree\_\_\_f}$.

DyckWord.outsidePartdefMathlib.Combinatorics.Enumerative.DyckWord, function or constant

Wording

no wording

English

Let $p$ be an element of $\mathrm{DyckWord}$. Then $\operatorname{outsidePart}$ applied to $p$ is an element of $\mathrm{DyckWord}$ defined as $\mathrm{dite}$ applied to $\EqtMACRoH {p}{0}$, the function that maps $h$ to $0$ and the function that maps $h_{1}$ to $\operatorname{drop}$ applied to $p$, $\operatorname{firstReturn} (p)+ 1$ and $\mathrm{DyckWord\_\_count\_take\_firstReturn\_add\_one}$ applied to $h_{1}$.

DyckWord.semilengthdefMathlib.Combinatorics.Enumerative.DyckWord, function or constant

Wording

no wording

English

Let $p$ be an element of $\mathrm{DyckWord}$. Then $\operatorname{semilength}$ applied to $p$ is a natural number defined as the multiplicity of $\operatorname{U}$ in the underlying list of $p$.

DyckWord.takedefMathlib.Combinatorics.Enumerative.DyckWord, function or constant

Wording

no wording

English

Let $p$ be an element of $\mathrm{DyckWord}$. Let $i$ be a natural number such that the multiplicity of $\operatorname{U}$ in $\operatorname{take}$ applied to $i$ and the underlying list of $p$ is equal to the multiplicity of $\operatorname{D}$ in $\operatorname{take}$ applied to $i$ and the underlying list of $p$. Then $\operatorname{take}$ applied to $p$, $i$ and $\mathrm{hi}$ is an element of $\mathrm{DyckWord}$.

DyckWord.toListdefMathlib.Combinatorics.Enumerative.DyckWord, function or constant

Wording

the underlying list of self (from the docstring)

English

Let $\mathrm{self}$ be an element of $\mathrm{DyckWord}$. Then the underlying list of $\mathrm{self}$ is a list of elements of $\mathrm{DyckStep}$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.

DyckWord.toTreedefMathlib.Combinatorics.Enumerative.DyckWord, function or constant

Wording

the tree of p (from the name)

English

Let $p$ be an element of $\mathrm{DyckWord}$. Then the tree of $p$ is a binary tree of $\mathrm{Unit}$.

instInhabitedDyckStep.defaultdefMathlib.Combinatorics.Enumerative.DyckWord, function or constant

Wording

the default (from the name)

English

The default is an element of $\mathrm{DyckStep}$ defined as $\operatorname{U}$.

Mathlib.Combinatorics.Enumerative.IncidenceAlgebra

IncidenceAlgebrastructureMathlib.Combinatorics.Enumerative.IncidenceAlgebra, type

Wording

incidence algebra of x and x1 (from the name)

English

Let $x$ and $x_{1}$ be sets. Then the incidence algebras of $x$ and $x_{1}$ are a basic type.

IncidenceAlgebra.eulerChardefMathlib.Combinatorics.Enumerative.IncidenceAlgebra, function or constant

Wording

the Euler characteristic of x and x1 (from the docstring)

English

Let $x$ and $x_{1}$ be sets. Then the Euler characteristic of $x$ and $x_{1}$ is an element of $x$ defined as $\operatorname{mu}$ applied to $x$, the bottom and the top.

IncidenceAlgebra.lambdadefMathlib.Combinatorics.Enumerative.IncidenceAlgebra, function or constant

Wording

the lambda function of the incidence algebra of x (from the docstring)

English

Let $x$ be a set. Then the lambda function of the incidence algebra of $x$ is an incidence algebra of $x$ and $x_{1}$.

IncidenceAlgebra.mudefMathlib.Combinatorics.Enumerative.IncidenceAlgebra, function or constant

Wording

no wording

English

Let $x$ be a set. Then $\operatorname{mu}$ applied to $x$ is an incidence algebra of $x$ and $x_{1}$.

IncidenceAlgebra.proddefMathlib.Combinatorics.Enumerative.IncidenceAlgebra, function or constant

Wording

the product of f and g (from the name)

English

Let $f$ be an incidence algebra of $x$ and $x_{1}$. Let $g$ be an incidence algebra of $x$ and $x_{2}$. Then the product of $f$ and $g$ is an incidence algebra of $x$ and $\mathrm{Prod}$ applied to $x_{1}$ and $x_{2}$.

IncidenceAlgebra.toFundefMathlib.Combinatorics.Enumerative.IncidenceAlgebra, function or constant

Wording

the incidence algebra of x4 and x5 (from the name)

English

Let $\mathrm{self}$ be an incidence algebra of $x$ and $x_{1}$. Let $x_{4}$ and $x_{5}$ be elements of $x_{1}$. Then the incidence algebra of $x_{4}$ and $x_{5}$ is an element of $x$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$, $x_{4}$ and $x_{5}$.

IncidenceAlgebra.zetadefMathlib.Combinatorics.Enumerative.IncidenceAlgebra, function or constant

Wording

the zeta function of the incidence algebra of x (from the docstring)

English

Let $x$ be a set. Then the zeta function of the incidence algebra of $x$ is an incidence algebra of $x$ and $x_{1}$.

Mathlib.Combinatorics.Enumerative.Partition.Basic

Nat.PartitionstructureMathlib.Combinatorics.Enumerative.Partition.Basic, type

Wording

partition of n (from the name)

English

Let $n$ be a natural number. Then the partitions of $n$ are a basic type.

Nat.Partition.countRestricteddefMathlib.Combinatorics.Enumerative.Partition.Basic, function or constant

Wording

no wording

English

Let $n$ and $m$ be elements of $\Natural$. Then $\operatorname{countRestricted}$ applied to $n$ and $m$ is a finite set of the set of partitions of $n$ defined as $\FinsetFilter {x}{\mathrm{forall} (\Natural , \lambda i . \mathrm{if} (\MembershipmemMACRoT {\operatorname{parts} (x)}{i}, \mathrm{Lt} (\operatorname{count} (i , \operatorname{parts} (x)), m)))}{\FinsetunivMACRoAC}$.

Nat.Partition.distinctsdefMathlib.Combinatorics.Enumerative.Partition.Basic, function or constant

Wording

the distinct of n (from the name)

English

Let $n$ be an element of $\Natural$. Then the distinct of $n$ is a finite set of the set of partitions of $n$ defined as $\FinsetFilter {c}{\operatorname{Nodup} (\operatorname{parts} (c))}{\FinsetunivMACRoAC}$.

Nat.Partition.indiscretedefMathlib.Combinatorics.Enumerative.Partition.Basic, function or constant

Wording

no wording

English

Let $n$ be a natural number. Then $\operatorname{indiscrete}$ applied to $n$ is a partition of $n$.

Nat.Partition.oddDistinctsdefMathlib.Combinatorics.Enumerative.Partition.Basic, function or constant

Wording

the odd distinct of n (from the name)

English

Let $n$ be a natural number. Then the odd distinct of $n$ is a finite set of the set of partitions of $n$ defined as $\operatorname{inter}$ applied to $\operatorname{odds}$ applied to $n$ and the distinct of $n$.

Nat.Partition.oddsdefMathlib.Combinatorics.Enumerative.Partition.Basic, function or constant

Wording

no wording

English

Let $n$ be a natural number. Then $\operatorname{odds}$ applied to $n$ is a finite set of the set of partitions of $n$ defined as $\operatorname{restricted}$ applied to $n$ and the function that maps $x$ to the proposition that $x$ is not even.

Nat.Partition.ofCompositiondefMathlib.Combinatorics.Enumerative.Partition.Basic, function or constant

Wording

the partition of n and c (from the name)

English

Let $n$ be a natural number. Let $c$ be a composition of $n$. Then the partition of $n$ and $c$ is a partition of $n$.

Nat.Partition.ofMultisetdefMathlib.Combinatorics.Enumerative.Partition.Basic, function or constant

Wording

the partition of l (from the name)

English

Let $l$ be a multiset of $\Natural$. Then the partition of $l$ is a partition of the sum of $l$.

Nat.Partition.ofSumsdefMathlib.Combinatorics.Enumerative.Partition.Basic, function or constant

Wording

the partition of n and l (from the name)

English

Let $n$ be a natural number. Let $l$ be a multiset of $\Natural$ such that the sum of $l$ is equal to $n$. Then the partition of $n$ and $l$ is a partition of $n$.

Nat.Partition.ofSymdefMathlib.Combinatorics.Enumerative.Partition.Basic, function or constant

Wording

the partition of s (from the name)

English

Let $s$ be a symmetric power of $x$ and $n$. Then the partition of $s$ is a partition of $n$.

Nat.Partition.ofSymShapeEquivdefMathlib.Combinatorics.Enumerative.Partition.Basic, function or constant

Wording

the partition of x4 and e (from the name)

English

Let $x_{4}$ be a partition of $n$. Let $e$ be an element of $\EquivMACRoAE {x}{x_{1}}$. Then the partition of $x_{4}$ and $e$ is an element of $\EquivMACRoAE {(\SubtypeSet {x_{5}}{(\EqtMACRoH {\operatorname{ofSym} (x_{5})}{x_{4}})})}{(\SubtypeSet {x_{6}}{(\EqtMACRoH {\operatorname{ofSym} (x_{6})}{x_{4}})})}$.

Nat.Partition.partitionWithPartEquivdefMathlib.Combinatorics.Enumerative.Partition.Basic, function or constant

Wording

the partition with part equivalence of ha1 and ha (from the name)

English

Assume that $1 \leq a$. Assume that $a \leq n$. Then the partition with part equivalence of $\mathrm{ha1}$ and $\mathrm{ha}$ is an element of $\EquivMACRoAE {(\SubtypeSet {p}{(\MembershipmemMACRoT {\operatorname{parts} (p)}{a})})}{\operatorname{Partition} (n - a)}$.

Nat.Partition.partsdefMathlib.Combinatorics.Enumerative.Partition.Basic, function or constant

Wording

the set of parts of self (from the name)

English

Let $\mathrm{self}$ be a partition of $n$. Then the set of parts of $\mathrm{self}$ is a multiset of $\Natural$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.

Nat.Partition.restricteddefMathlib.Combinatorics.Enumerative.Partition.Basic, function or constant

Wording

no wording

English

Let $n$ be an element of $\Natural$. Let $p$ be a function from elements of $\Natural$ to propositions. Then $\operatorname{restricted}$ applied to $n$ and $p$ is a finite set of the set of partitions of $n$ defined as $\FinsetFilter {x_{1}}{\mathrm{forall} (\Natural , \lambda i . \mathrm{if} (\MembershipmemMACRoT {\operatorname{parts} (x_{1})}{i}, p (i)))}{\FinsetunivMACRoAC}$.

Nat.Partition.toFinsuppAntidiagdefMathlib.Combinatorics.Enumerative.Partition.Basic, function or constant

Wording

no wording

English

Let $p$ be a partition of $n$. Then $\operatorname{toFinsuppAntidiag}$ applied to $p$ is an element of $\FinsuppMACRoQ {\Natural}{\Natural}$.

Mathlib.Combinatorics.Enumerative.Partition.GenFun

Nat.Partition.genFundefMathlib.Combinatorics.Enumerative.Partition.GenFun, function or constant

Wording

the generator function of f (from the name)

English

Let $f$ be a function from elements of $\Natural$ and elements of $\Natural$ to elements of $R$. Then the generator function of $f$ is a power series of $R$ defined as $\operatorname{mk}$ applied to the function that maps $n$ to $\FinsetSum {\FinsetunivMACRoAC}{p}{(\FinsuppProd {\operatorname{toFinsupp} (\operatorname{parts} (p))}{x_{1}}{x_{2}}{f (x_{1} , x_{2})})}$.

Mathlib.Combinatorics.Enumerative.Partition.YoungDiagram

Nat.Partition.conjugatedefMathlib.Combinatorics.Enumerative.Partition.YoungDiagram, function or constant

Wording

the conjugate of p (from the name)

English

Let $p$ be a partition of $n$. Then the conjugate of $p$ is a partition of $n$.

YoungDiagram.equivPartitiondefMathlib.Combinatorics.Enumerative.Partition.YoungDiagram, function or constant

Wording

the equivalence partition (from the name)

English

The equivalence partition is an element of $\EquivMACRoAE {(\SubtypeSet {x}{\mathrm{Eq} (\operatorname{card} (x), n)})}{\operatorname{Partition} (n)}$.

YoungDiagram.ofPartitiondefMathlib.Combinatorics.Enumerative.Partition.YoungDiagram, function or constant

Wording

no wording

English

Let $p$ be a partition of $n$. Then $\operatorname{ofPartition}$ applied to $p$ is an element of $\mathrm{YoungDiagram}$.

YoungDiagram.toPartitiondefMathlib.Combinatorics.Enumerative.Partition.YoungDiagram, function or constant

Wording

the partition of x and h (from the name)

English

Let $x$ be an element of $\mathrm{YoungDiagram}$ such that the cardinality of $x$ is equal to $n$. Then the partition of $x$ and $h$ is a partition of $n$.

Mathlib.Combinatorics.Enumerative.Pentagonal.Basic

pentagonaldefMathlib.Combinatorics.Enumerative.Pentagonal.Basic, function or constant

Wording

no wording

English

Let $k$ be an integer. Then $\mathrm{pentagonal}$ applied to $k$ is a natural number defined as $\operatorname{toNat}$ applied to $\frac{ k \times (3 \times k - 1)}{2}$.

Mathlib.Combinatorics.Enumerative.Pentagonal.EulerFunction

eulerFunctiondefMathlib.Combinatorics.Enumerative.Pentagonal.EulerFunction, function or constant

Wording

the Euler function of x1 (from the name)

English

Let $x_{1}$ be an element of $R$. Then the Euler function of $x_{1}$ is an element of $R$ defined as the sum of the function that maps $n$ to the product of $\operatorname{coeff}$ applied to $n$ and the pentagonal series of $R$ and $x_{1} ^ {n}$ and $\operatorname{unconditional}$ applied to $\Natural$.

Mathlib.Combinatorics.Enumerative.Pentagonal.PowerSeries

PowerSeries.pentagonalSeriesdefMathlib.Combinatorics.Enumerative.Pentagonal.PowerSeries, function or constant

Wording

the pentagonal series of R (from the name)

English

Let $R$ be a set. Then the pentagonal series of $R$ is a power series of $R$ defined as $\operatorname{mk}$ applied to the function that maps $n$ to $\mathrm{dite}$ applied to the proposition that there exists an integer $k$, such that $\mathrm{pentagonal} (k)= n$, the function that maps $h$ to the underlying value in the base of the negation one power of $\operatorname{choose}$ applied to $h$ and the function that maps $h_{1}$ to $0$.

Mathlib.Combinatorics.Enumerative.Schroder

Nat.largeSchroderdefMathlib.Combinatorics.Enumerative.Schroder, function or constant

Wording

the large Schroder of x (from the name)

English

Let $x$ be a natural number. Then the large Schroder of $x$ is a natural number.

Nat.smallSchroderdefMathlib.Combinatorics.Enumerative.Schroder, function or constant

Wording

the small Schroder of x (from the name)

English

Let $x$ be a natural number. Then the small Schroder of $x$ is a natural number.

Mathlib.Combinatorics.Enumerative.Stirling

Nat.stirlingFirstdefMathlib.Combinatorics.Enumerative.Stirling, function or constant

Wording

no wording

English

Let $x$ and $x_{1}$ be natural numbers. Then $\operatorname{stirlingFirst}$ applied to $x$ and $x_{1}$ is a natural number defined as $\operatorname{brecOn}$ applied to $x$, $\mathrm{Nat\_\_stirlingFirst\_\_\_f}$ and $x_{1}$.

Nat.stirlingSeconddefMathlib.Combinatorics.Enumerative.Stirling, function or constant

Wording

the Stirling number of the second kind of x and x1 (from the docstring)

English

Let $x$ and $x_{1}$ be natural numbers. Then the Stirling number of the second kind of $x$ and $x_{1}$ is a natural number defined as $\operatorname{brecOn}$ applied to $x$, $\mathrm{Nat\_\_stirlingSecond\_\_\_f}$ and $x_{1}$.

Mathlib.Combinatorics.Extremal.RuzsaSzemeredi

ruzsaSzemerediNumberdefMathlib.Combinatorics.Extremal.RuzsaSzemeredi, function or constant

Wording

no wording

English

generation took over the time limit

ruzsaSzemerediNumberNatdefMathlib.Combinatorics.Extremal.RuzsaSzemeredi, function or constant

Wording

no wording

English

Let $n$ be a natural number. Then $\mathrm{ruzsaSzemerediNumberNat}$ applied to $n$ is a natural number defined as $\mathrm{ruzsaSzemerediNumber}$ applied to $\mathrm{Fin}$ applied to $n$.

Mathlib.Combinatorics.Graph.Basic

GraphstructureMathlib.Combinatorics.Graph.Basic, type

Wording

graph of x and x1 (from the name)

English

Let $x$ and $x_{1}$ be sets. Then the graphs of $x$ and $x_{1}$ are a basic type.

Graph.AdjdefMathlib.Combinatorics.Graph.Basic, predicate

Wording

no wording

English

Let $G$ be a graph of $x$ and $x_{1}$. Let $x_{2}$ and $y$ be elements of $x$. Then $\operatorname{Adj}$ holds for $G$, $x_{2}$ and $y$, if there exists an element $e$ of $x_{1}$, such that $\operatorname{IsLink}$ holds for $G$, $e$, $x_{2}$ and $y$.

Graph.CompatibledefMathlib.Combinatorics.Graph.Basic, predicate

Wording

no wording

English

Let $G$ and $H$ be graphs of $x$ and $x_{1}$. Then $\operatorname{Compatible}$ holds for $G$ and $H$, if for all elements $e$ of $x_{1}$, if $e$ is an element of the edge set of $G$, then if $e$ is an element of the edge set of $H$, then for all elements $x_{2}$ and $y$ of $x$, $\operatorname{IsLink}$ holds for $G$, $e$, $x_{2}$ and $y$, if and only if $\operatorname{IsLink}$ holds for $H$, $e$, $x_{2}$ and $y$.

Graph.IncdefMathlib.Combinatorics.Graph.Basic, predicate

Wording

no wording

English

Let $G$ be a graph of $x$ and $x_{1}$. Let $e$ be an element of $x_{1}$. Let $x_{2}$ be an element of $x$. Then $\operatorname{Inc}$ holds for $G$, $e$ and $x_{2}$, if there exists an element $y$ of $x$, such that $\operatorname{IsLink}$ holds for $G$, $e$, $x_{2}$ and $y$.

Graph.Inc.otherdefMathlib.Combinatorics.Graph.Basic, function or constant

Wording

the other of h (from the name)

English

Assume that $\operatorname{Inc}$ holds for $G$, $e$ and $x_{2}$. Then the other of $h$ is an element of $x$ defined as $\operatorname{choose}$ applied to $h$.

Graph.IsLinkdefMathlib.Combinatorics.Graph.Basic, predicate

Wording

no wording

English

Let $\mathrm{self}$ be a graph of $x$ and $x_{1}$. Let $x_{2}$ be an element of $x_{1}$. Let $x_{3}$ and $x_{4}$ be elements of $x$. Then $\operatorname{IsLink}$ holds for $\mathrm{self}$, $x_{2}$, $x_{3}$ and $x_{4}$, if $\operatorname{proj1}$ holds for $\mathrm{self}$, $x_{2}$, $x_{3}$ and $x_{4}$.

Graph.IsLoopAtdefMathlib.Combinatorics.Graph.Basic, predicate

Wording

no wording

English

Let $G$ be a graph of $x$ and $x_{1}$. Let $e$ be an element of $x_{1}$. Let $x_{2}$ be an element of $x$. Then $\operatorname{IsLoopAt}$ holds for $G$, $e$ and $x_{2}$, if $\operatorname{IsLink}$ holds for $G$, $e$, $x_{2}$ and $x_{2}$.

Graph.IsNonloopAtdefMathlib.Combinatorics.Graph.Basic, predicate

Wording

no wording

English

Let $G$ be a graph of $x$ and $x_{1}$. Let $e$ be an element of $x_{1}$. Let $x_{2}$ be an element of $x$. Then $\operatorname{IsNonloopAt}$ holds for $G$, $e$ and $x_{2}$, if there exists an element $y$ of $x$, such that $y \neq x_{2}$ and $\operatorname{IsLink}$ holds for $G$, $e$, $x_{2}$ and $y$.

Graph.bananadefMathlib.Combinatorics.Graph.Basic, function or constant

Wording

no wording

English

Let $u$ and $v$ be elements of $x$. Let $\mathrm{edgeSet}$ be an element of $\wp x_{1}$. Then $\operatorname{banana}$ applied to $u$, $v$ and $\mathrm{edgeSet}$ is a graph of $x$ and $x_{1}$.

Graph.bouquetdefMathlib.Combinatorics.Graph.Basic, function or constant

Wording

the bouquet of v and edgeSet (from the name)

English

Let $v$ be an element of $x$. Let $\mathrm{edgeSet}$ be an element of $\wp x_{1}$. Then the bouquet of $v$ and $\mathrm{edgeSet}$ is a graph of $x$ and $x_{1}$ defined as $\operatorname{banana}$ applied to $v$, $v$ and $\mathrm{edgeSet}$.

Graph.copydefMathlib.Combinatorics.Graph.Basic, function or constant

Wording

the copy of G (from the name)

English

Let $G$ be a graph of $x$ and $x_{1}$ such that the vertex set of $G$ is equal to $\mathrm{vertexSet}$, the edge set of $G$ is equal to $\mathrm{edgeSet}$ and for all elements $e$ of $x_{1}$, for all elements $x_{2}$ of $x$, for all elements $y$ of $x$, $\operatorname{IsLink}$ holds for $G$, $e$, $x_{2}$ and $y$, if and only if $\mathrm{IsLink}$ holds for $e$, $x_{2}$ and $y$. Then the copy of $G$ is a graph of $x$ and $x_{1}$.

Graph.edgeSetdefMathlib.Combinatorics.Graph.Basic, function or constant

Wording

the edge set of self (from the docstring)

English

Let $\mathrm{self}$ be a graph of $x$ and $x_{1}$. Then the edge set of $\mathrm{self}$ is an element of $\wp x_{1}$ defined as $\operatorname{proj2}$ applied to $\mathrm{self}$.

Graph.incidenceSetdefMathlib.Combinatorics.Graph.Basic, function or constant

Wording

the incidence set of x2 (from the name)

English

Let $x_{2}$ be an element of $x$. Then the incidence set of $x_{2}$ is an element of $\wp x_{1}$ defined as $\operatorname{ofPred}$ applied to the function that maps $e$ to $\operatorname{Inc}$ applied to $G$, $e$ and $x_{2}$.

Graph.loopSetdefMathlib.Combinatorics.Graph.Basic, function or constant

Wording

the loop set of x2 (from the name)

English

Let $x_{2}$ be an element of $x$. Then the loop set of $x_{2}$ is an element of $\wp x_{1}$ defined as $\operatorname{ofPred}$ applied to the function that maps $e$ to $\operatorname{IsLoopAt}$ applied to $G$, $e$ and $x_{2}$.

Graph.noEdgedefMathlib.Combinatorics.Graph.Basic, function or constant

Wording

no wording

English

Let $\mathrm{vertexSet}$ be an element of $\wp x$. Let $x_{1}$ be a set. Then $\operatorname{noEdge}$ applied to $\mathrm{vertexSet}$ and $x_{1}$ is a graph of $x$ and $x_{1}$.

Graph.vertexSetdefMathlib.Combinatorics.Graph.Basic, function or constant

Wording

the vertex set of self (from the docstring)

English

Let $\mathrm{self}$ be a graph of $x$ and $x_{1}$. Then the vertex set of $\mathrm{self}$ is an element of $\wp x$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.

Mathlib.Combinatorics.Graph.Connected.EdgeCut

Graph.IsBonddefMathlib.Combinatorics.Graph.Connected.EdgeCut, predicate

Wording

no wording

English

Let $G$ be a graph of $x$ and $x_{1}$. Let $F$ be an element of $\wp x_{1}$. Then $\operatorname{IsBond}$ holds for $G$ and $F$, if $F$ is minimal with respect to the function that maps $F_{1}$ to the proposition that $G$ is an edge cut and $F_{1}$ is nonempty.

Graph.IsBridgedefMathlib.Combinatorics.Graph.Connected.EdgeCut, predicate

Wording

no wording

English

Let $G$ be a graph of $x$ and $x_{1}$. Let $e$ be an element of $x_{1}$. Then $\operatorname{IsBridge}$ holds for $G$ and $e$, if $G$ is an edge cut.

Graph.IsEdgeCutdefMathlib.Combinatorics.Graph.Connected.EdgeCut, predicate

Wording

G is an edge cut (from the docstring)

English

Let $G$ be a graph of $x$ and $x_{1}$. Let $F$ be an element of $\wp x_{1}$. Then $G$ is an edge cut, if there exists an element $S$ of $\wp x$, such that the edge cut of $G$ and $S$ is equal to $F$.

Graph.edgeCutdefMathlib.Combinatorics.Graph.Connected.EdgeCut, function or constant

Wording

the edge cut of G and S (from the docstring)

English

Let $G$ be a graph of $x$ and $x_{1}$. Let $S$ be an element of $\wp x$. Then the edge cut of $G$ and $S$ is an element of $\wp x_{1}$ defined as $\operatorname{ofPred}$ applied to the function that maps $e$ to the proposition that there exist elements $u$ and $v$ of $x$, such that $\operatorname{IsLink}$ holds for $G$, $e$, $u$ and $v$, $u$ is an element of $S$ and $v$ is not an element of $S$.

Mathlib.Combinatorics.Graph.Delete

Graph.deleteEdgesdefMathlib.Combinatorics.Graph.Delete, function or constant

Wording

no wording

English

Let $G$ be a graph of $x$ and $x_{1}$. Let $F$ be an element of $\wp x_{1}$. Then $\operatorname{deleteEdges}$ applied to $G$ and $F$ is a graph of $x$ and $x_{1}$.

Graph.deleteVertsdefMathlib.Combinatorics.Graph.Delete, function or constant

Wording

no wording

English

Let $G$ be a graph of $x$ and $x_{1}$. Let $X$ be an element of $\wp x$. Then $\operatorname{deleteVerts}$ applied to $G$ and $X$ is a graph of $x$ and $x_{1}$ defined as $\operatorname{induce}$ applied to $G$ and $\operatorname{sdiff}$ applied to the vertex set of $G$ and $X$.

Graph.inducedefMathlib.Combinatorics.Graph.Delete, function or constant

Wording

no wording

English

Let $G$ be a graph of $x$ and $x_{1}$. Let $X$ be an element of $\wp x$. Then $\operatorname{induce}$ applied to $G$ and $X$ is a graph of $x$ and $x_{1}$.

Graph.restrictdefMathlib.Combinatorics.Graph.Delete, function or constant

Wording

no wording

English

Let $G$ be a graph of $x$ and $x_{1}$. Let $x_{2}$ be an element of $\wp x_{1}$. Then $\operatorname{restrict}$ applied to $G$ and $x_{2}$ is a graph of $x$ and $x_{1}$.

Mathlib.Combinatorics.Graph.Maps

Graph.mapdefMathlib.Combinatorics.Graph.Maps, function or constant

Wording

the map of f and G (from the name)

English

Let $f$ be a function from elements of $x$ to elements of $x_{1}$. Let $G$ be a graph of $x$ and $x_{2}$. Then the map of $f$ and $G$ is a graph of $x_{1}$ and $x_{2}$.

Mathlib.Combinatorics.Graph.Simple

Graph.LooplessclassMathlib.Combinatorics.Graph.Simple, predicate

Wording

no wording

English

Let $G$ be a graph of $x$ and $x_{1}$. Then we can say that $\operatorname{Loopless}$ holds for $G$.

Graph.SimpleclassMathlib.Combinatorics.Graph.Simple, predicate

Wording

G is simple (from the name)

English

Let $G$ be a graph of $x$ and $x_{1}$. Then we can say that $G$ is simple.

Graph.ofSimpleGraphdefMathlib.Combinatorics.Graph.Simple, function or constant

Wording

the graph of G (from the name)

English

Let $G$ be a simple graph of $x$. Then the graph of $G$ is a graph of $x$ and the set of symmetric squares of $x$.

Graph.toSimpleGraphdefMathlib.Combinatorics.Graph.Simple, function or constant

Wording

the simple graph of G (from the name)

English

Let $G$ be a graph of $x$ and $x_{1}$. Then the simple graph of $G$ is a simple graph of the set of elements of the vertex set of $G$.

Graph.toSimpleGraphOfSimpleGraphIsodefMathlib.Combinatorics.Graph.Simple, function or constant

Wording

the simple graph of G (from the name)

English

Let $G$ be a simple graph of $x$. Then the simple graph of $G$ is an isomorphism of the simple graph of the graph of $G$ and $G$.

Mathlib.Combinatorics.Graph.Subgraph

Graph.IsClosedSubgraphstructureMathlib.Combinatorics.Graph.Subgraph, predicate

Wording

no wording

English

Let $H$ and $G$ be graphs of $x$ and $x_{1}$. Then we can say that $\operatorname{IsClosedSubgraph}$ holds for $H$ and $G$.

Graph.IsInducedSubgraphstructureMathlib.Combinatorics.Graph.Subgraph, predicate

Wording

no wording

English

Let $H$ and $G$ be graphs of $x$ and $x_{1}$. Then we can say that $\operatorname{IsInducedSubgraph}$ holds for $H$ and $G$.

Graph.IsSpanningSubgraphstructureMathlib.Combinatorics.Graph.Subgraph, predicate

Wording

no wording

English

Let $H$ and $G$ be graphs of $x$ and $x_{1}$. Then we can say that $\operatorname{IsSpanningSubgraph}$ holds for $H$ and $G$.

Graph.IsSubgraphstructureMathlib.Combinatorics.Graph.Subgraph, predicate

Wording

no wording

English

Let $H$ and $G$ be graphs of $x$ and $x_{1}$. Then we can say that $\operatorname{IsSubgraph}$ holds for $H$ and $G$.

Mathlib.Combinatorics.HalesJewett

Combinatorics.LinestructureMathlib.Combinatorics.HalesJewett, type

Wording

line of x and x1 (from the name)

English

Let $x$ and $x_{1}$ be sets. Then the lines of $x$ and $x_{1}$ are a basic type.

Combinatorics.Line.AlmostMonostructureMathlib.Combinatorics.HalesJewett, type

Wording

no wording

English

Let $C$ be a function from functions from elements of $x_{1}$ to elements of $\mathrm{Option}$ applied to $x$ to elements of $x_{2}$. Then the elements of $\operatorname{AlmostMono}$ applied to $C$ are a basic type.

Combinatorics.Line.AlmostMono.colordefMathlib.Combinatorics.HalesJewett, function or constant

Wording

no wording

English

Let $\mathrm{self}$ be an element of $\operatorname{AlmostMono}$ applied to $C$. Then $\operatorname{color}$ applied to $\mathrm{self}$ is an element of $x_{2}$ defined as $\operatorname{proj1}$ applied to $\mathrm{self}$.

Combinatorics.Line.AlmostMono.linedefMathlib.Combinatorics.HalesJewett, function or constant

Wording

the underlying line of self (from the docstring)

English

Let $\mathrm{self}$ be an element of $\operatorname{AlmostMono}$ applied to $C$. Then the underlying line of $\mathrm{self}$ is a line of $\mathrm{Option}$ applied to $x$ and $x_{1}$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.

Combinatorics.Line.ColorFocusedstructureMathlib.Combinatorics.HalesJewett, type

Wording

no wording

English

Let $C$ be a function from functions from elements of $x_{1}$ to elements of $\mathrm{Option}$ applied to $x$ to elements of $x_{2}$. Then the elements of $\operatorname{ColorFocused}$ applied to $C$ are a basic type.

Combinatorics.Line.ColorFocused.focusdefMathlib.Combinatorics.HalesJewett, function or constant

Wording

the focus of self and x3 (from the name)

English

Let $\mathrm{self}$ be an element of $\operatorname{ColorFocused}$ applied to $C$. Let $x_{3}$ be an element of $x_{1}$. Then the focus of $\mathrm{self}$ and $x_{3}$ is an element of $\mathrm{Option}$ applied to $x$ defined as $\operatorname{proj1}$ applied to $\mathrm{self}$ and $x_{3}$.

Combinatorics.Line.ColorFocused.linesdefMathlib.Combinatorics.HalesJewett, function or constant

Wording

the line of self (from the name)

English

Let $\mathrm{self}$ be an element of $\operatorname{ColorFocused}$ applied to $C$. Then the line of $\mathrm{self}$ is a multiset of $\operatorname{AlmostMono}$ applied to $C$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.

Combinatorics.Line.IsMonodefMathlib.Combinatorics.HalesJewett, predicate

Wording

C is monochromatic (from the docstring)

English

Let $C$ be a function from functions from elements of $x_{1}$ to elements of $x$ to elements of $x_{2}$. Let $l$ be a line of $x$ and $x_{1}$. Then $C$ is monochromatic, if there exists an element $c$ of $x_{2}$, such that for all elements $x_{3}$ of $x$, $C$ applied to $\operatorname{toFun}$ applied to $x_{3}$ is equal to $c$.

Combinatorics.Line.diagonaldefMathlib.Combinatorics.HalesJewett, function or constant

Wording

the diagonal line of x and x1 (from the docstring)

English

Let $x$ and $x_{1}$ be sets. Then the diagonal line of $x$ and $x_{1}$ is a line of $x$ and $x_{1}$.

Combinatorics.Line.horizontaldefMathlib.Combinatorics.HalesJewett, function or constant

Wording

no wording

English

Let $l$ be a line of $x$ and $x_{1}$. Let $v$ be a function from elements of $x_{2}$ to elements of $x$. Then $\operatorname{horizontal}$ applied to $l$ and $v$ is a line of $x$ and $\mathrm{Sum}$ applied to $x_{1}$ and $x_{2}$.

Combinatorics.Line.idxFundefMathlib.Combinatorics.HalesJewett, function or constant

Wording

the index function of self and x2 (from the name)

English

Let $\mathrm{self}$ be a line of $x$ and $x_{1}$. Let $x_{2}$ be an element of $x_{1}$. Then the index function of $\mathrm{self}$ and $x_{2}$ is an element of $\mathrm{Option}$ applied to $x$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$ and $x_{2}$.

Combinatorics.Line.mapdefMathlib.Combinatorics.HalesJewett, function or constant

Wording

the map of f and l (from the name)

English

Let $f$ be a function from elements of $x$ to elements of $x_{1}$. Let $l$ be a line of $x$ and $x_{2}$. Then the map of $f$ and $l$ is a line of $x_{1}$ and $x_{2}$.

Combinatorics.Line.proddefMathlib.Combinatorics.HalesJewett, function or constant

Wording

the product of l and #2 (from the name)

English

Let $l$ be a line of $x$ and $x_{1}$. Let $\mathrm{l'}$ be a line of $x$ and $x_{2}$. Then the product of $l$ and $\mathrm{l'}$ is a line of $x$ and $\mathrm{Sum}$ applied to $x_{1}$ and $x_{2}$.

Combinatorics.Line.toFundefMathlib.Combinatorics.HalesJewett, function or constant

Wording

the line of x2 and i (from the name)

English

Let $l$ be a line of $x$ and $x_{1}$. Let $x_{2}$ be an element of $x$. Let $i$ be an element of $x_{1}$. Then the line of $x_{2}$ and $i$ is an element of $x$ defined as $\operatorname{getD}$ applied to the index function of $l$ and $i$ and $x_{2}$.

Combinatorics.Line.toSubspacedefMathlib.Combinatorics.HalesJewett, function or constant

Wording

the subspace of l (from the name)

English

Let $l$ be a line of the set of functions from elements of $x$ to elements of $x_{1}$ and $x_{2}$. Then the subspace of $l$ is a subspace of $x_{1}$ and $\mathrm{Prod}$ applied to $x_{2}$ and $x$.

Combinatorics.Line.toSubspaceUnitdefMathlib.Combinatorics.HalesJewett, function or constant

Wording

the subspace unit of l (from the name)

English

Let $l$ be a line of $x$ and $x_{1}$. Then the subspace unit of $l$ is a subspace of $x$ and $x_{1}$.

Combinatorics.Line.verticaldefMathlib.Combinatorics.HalesJewett, function or constant

Wording

no wording

English

Let $v$ be a function from elements of $x_{1}$ to elements of $x$. Let $l$ be a line of $x$ and $x_{2}$. Then $\operatorname{vertical}$ applied to $v$ and $l$ is a line of $x$ and $\mathrm{Sum}$ applied to $x_{1}$ and $x_{2}$.

Combinatorics.SubspacestructureMathlib.Combinatorics.HalesJewett, type

Wording

subspace of x1 and x2 (from the name)

English

Let $x$, $x_{1}$ and $x_{2}$ be sets. Then the subspaces of $x_{1}$ and $x_{2}$ are a basic type.

Combinatorics.Subspace.IsMonodefMathlib.Combinatorics.HalesJewett, predicate

Wording

no wording

English

Let $C$ be a function from functions from elements of $x_{2}$ to elements of $x_{1}$ to elements of $x_{3}$. Let $l$ be a subspace of $x_{1}$ and $x_{2}$. Then $\operatorname{IsMono}$ holds for $C$ and $l$, if there exists an element $c$ of $x_{3}$, such that for all functions $x_{4}$ from elements of $x$ to elements of $x_{1}$, $C$ applied to $\operatorname{toFun}$ applied to $x_{4}$ is equal to $c$.

Combinatorics.Subspace.idxFundefMathlib.Combinatorics.HalesJewett, function or constant

Wording

the index function of self and x3 (from the name)

English

Let $\mathrm{self}$ be a subspace of $x_{1}$ and $x_{2}$. Let $x_{3}$ be an element of $x_{2}$. Then the index function of $\mathrm{self}$ and $x_{3}$ is an element of $\mathrm{Sum}$ applied to $x_{1}$ and $x$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$ and $x_{3}$.

Combinatorics.Subspace.reindexdefMathlib.Combinatorics.HalesJewett, function or constant

Wording

the reindexing of x7 and x8 (from the name)

English

Let $l$ be a subspace of $x_{1}$ and $x_{2}$. Let $x_{6}$ be an equivalence from $x$ to $x_{3}$. Let $x_{7}$ be an equivalence from $x_{1}$ to $x_{4}$. Let $x_{8}$ be an equivalence from $x_{2}$ to $x_{5}$. Then the reindexing of $x_{7}$ and $x_{8}$ is a subspace of $x_{4}$ and $x_{5}$.

Combinatorics.Subspace.toFundefMathlib.Combinatorics.HalesJewett, function or constant

Wording

the subspace of x3 and i (from the name)

English

Let $l$ be a subspace of $x_{1}$ and $x_{2}$. Let $x_{3}$ be a function from elements of $x$ to elements of $x_{1}$. Let $i$ be an element of $x_{2}$. Then the subspace of $x_{3}$ and $i$ is an element of $x_{1}$ defined as $\operatorname{elim}$ applied to $\mathrm{id}$, $x_{3}$ and the index function of $l$ and $i$.

Mathlib.Combinatorics.Hall.Basic

hallMatchingsFunctordefMathlib.Combinatorics.Hall.Basic, function or constant

Wording

the Hall matching functor of t (from the name)

English

Let $t$ be a function from elements of $x$ to finite sets of $x_{1}$. Then the Hall matching functor of $t$ is a functor of the set of opposites of the set of finite sets of $x$ and the set of sets.

hallMatchingsOndefMathlib.Combinatorics.Hall.Basic, function or constant

Wording

no wording

English

Let $t$ be a function from elements of $x$ to finite sets of $x_{1}$. Let $x_{2}$ be a finite set of $x$. Then $\mathrm{hallMatchingsOn}$ applied to $t$ and $x_{2}$ is an element of $\wp (\mathrm{Elem} (\SubtypeSet {x_{4}}{(\MembershipmemMACRoT {x_{2}}{x_{4}})})\rightarrow x_{1})$ defined as $\operatorname{ofPred}$ applied to the function that maps $f$ to the proposition that $f$ is injective and for all elements $x_{3}$ of $\SubtypeSet {x_{4}}{(\MembershipmemMACRoT {x_{2}}{x_{4}})}$, $\MembershipmemMACRoT {t (x_{3})}{f (x_{3})}$.

hallMatchingsOn.restrictdefMathlib.Combinatorics.Hall.Basic, function or constant

Wording

no wording

English

Let $t$ be a function from elements of $x$ to finite sets of $x_{1}$. Assume that $x_{2} \leq x_{3}$. Let $f$ be an element of $\mathrm{hallMatchingsOn}$ applied to $t$ and $x_{3}$. Then $\operatorname{restrict}$ applied to $t$, $h$ and $f$ is an element of $\mathrm{hallMatchingsOn}$ applied to $t$ and $x_{2}$ defined as the function that maps $i$ to $i$.

Mathlib.Combinatorics.Hindman

Hindman.FPinductiveMathlib.Combinatorics.Hindman, predicate

Wording

no wording

English

Let $x_{1}$ be an element of $\mathrm{Stream'}$ applied to $M$. Let $x_{2}$ be an element of $M$. Then we can say that $\operatorname{FP}$ holds for $x_{1}$ and $x_{2}$.

Hindman.FP.belowinductiveMathlib.Combinatorics.Hindman, predicate

Wording

no wording

English

Assume that $\operatorname{FP}$ holds for $x_{1}$ and $x_{2}$. Then we can say that $\operatorname{below}$ holds for $t$.

Hindman.FSinductiveMathlib.Combinatorics.Hindman, predicate

Wording

no wording

English

Let $x_{1}$ be an element of $\mathrm{Stream'}$ applied to $M$. Let $x_{2}$ be an element of $M$. Then we can say that $\operatorname{FS}$ holds for $x_{1}$ and $x_{2}$.

Hindman.FS.belowinductiveMathlib.Combinatorics.Hindman, predicate

Wording

no wording

English

Assume that $\operatorname{FS}$ holds for $x_{1}$ and $x_{2}$. Then we can say that $\operatorname{below}$ holds for $t$.

Mathlib.Combinatorics.Hypergraph.Basic

HypergraphstructureMathlib.Combinatorics.Hypergraph.Basic, type

Wording

hypergraph of x (from the name)

English

Let $x$ be a set. Then the hypergraphs of $x$ are a basic type.

Hypergraph.AdjdefMathlib.Combinatorics.Hypergraph.Basic, predicate

Wording

no wording

English

Let $H$ be a hypergraph of $x$. Let $x_{1}$ and $y$ be elements of $x$. Then $\operatorname{Adj}$ holds for $H$, $x_{1}$ and $y$, if there exists an element $e$ of $\wp x$, such that $e$ is an element of the edge set of $H$, $x_{1}$ is an element of $e$ and $y$ is an element of $e$.

Hypergraph.EAdjdefMathlib.Combinatorics.Hypergraph.Basic, predicate

Wording

no wording

English

Let $H$ be a hypergraph of $x$. Let $e$ and $f$ be elements of $\wp x$. Then $\operatorname{EAdj}$ holds for $H$, $e$ and $f$, if $e$ is an element of the edge set of $H$, $f$ is an element of the edge set of $H$ and there exists an element $x_{1}$ of $x$ such that $x_{1}$ is an element of $e$ and $x_{1}$ is an element of $f$.

Hypergraph.IsCompletedefMathlib.Combinatorics.Hypergraph.Basic, predicate

Wording

H is complete (from the docstring)

English

Let $H$ be a hypergraph of $x$. Then $H$ is complete, if for all elements $e$ of $\wp x$, if $e$ is less than or equal to the vertex set of $H$, then $e$ is an element of the edge set of $H$.

Hypergraph.IsIsolateddefMathlib.Combinatorics.Hypergraph.Basic, predicate

Wording

H is isolated (from the docstring)

English

Let $H$ be a hypergraph of $x$. Let $x_{1}$ be an element of $x$. Then $H$ is isolated, if for all elements $e$ of $\wp x$, if $e$ is an element of the edge set of $H$, then $x_{1}$ is not an element of $e$.

Hypergraph.IsLineardefMathlib.Combinatorics.Hypergraph.Basic, predicate

Wording

H is linear (from the docstring)

English

Let $H$ be a hypergraph of $x$. Then $H$ is linear, if $\operatorname{Pairwise}$ holds for the edge set of $H$ and the function that maps $e$ and $\mathrm{e'}$ to the proposition that $\operatorname{inter}$ applied to $e$ and $\mathrm{e'}$ is a subsingleton.

Hypergraph.IsLoopdefMathlib.Combinatorics.Hypergraph.Basic, predicate

Wording

no wording

English

Let $H$ be a hypergraph of $x$. Let $e$ be an element of $\wp x$. Then $\operatorname{IsLoop}$ holds for $H$ and $e$, if $e$ is an element of the edge set of $H$ and there exists an element $x_{1}$ of $x$ such that $\EqtMACRoH {e}{\operatorname{singleton} (x_{1})}$.

Hypergraph.IsNonemptydefMathlib.Combinatorics.Hypergraph.Basic, predicate

Wording

H is nonempty (from the docstring)

English

Let $H$ be a hypergraph of $x$. Then $H$ is nonempty, if the vertex set of $H$ or the edge set of $H$ is nonempty.

Hypergraph.IsTrivialdefMathlib.Combinatorics.Hypergraph.Basic, predicate

Wording

H is trivial (from the docstring)

English

Let $H$ be a hypergraph of $x$. Then $H$ is trivial, if the vertex set of $H$ is nonempty and the edge set of $H$ is equal to $\operatorname{emptyCollection}$.

Hypergraph.completeOndefMathlib.Combinatorics.Hypergraph.Basic, function or constant

Wording

no wording

English

Let $f$ be an element of $\wp x$. Then $\operatorname{completeOn}$ applied to $f$ is a hypergraph of $x$.

Hypergraph.edgeSetdefMathlib.Combinatorics.Hypergraph.Basic, function or constant

Wording

the edge set of self (from the docstring)

English

Let $\mathrm{self}$ be a hypergraph of $x$. Then the edge set of $\mathrm{self}$ is an element of $\wp (\wp x)$ defined as $\operatorname{proj1}$ applied to $\mathrm{self}$.

Hypergraph.imagedefMathlib.Combinatorics.Hypergraph.Basic, function or constant

Wording

the image of H and f (from the name)

English

Let $H$ be a hypergraph of $x$. Let $f$ be a function from elements of $x$ to elements of $x_{1}$. Then the image of $H$ and $f$ is a hypergraph of $x_{1}$.

Hypergraph.trivialOndefMathlib.Combinatorics.Hypergraph.Basic, function or constant

Wording

no wording

English

Let $f$ be an element of $\wp x$. Then $\operatorname{trivialOn}$ applied to $f$ is a hypergraph of $x$.

Hypergraph.vertexSetdefMathlib.Combinatorics.Hypergraph.Basic, function or constant

Wording

the vertex set of self (from the docstring)

English

Let $\mathrm{self}$ be a hypergraph of $x$. Then the vertex set of $\mathrm{self}$ is an element of $\wp x$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.

Mathlib.Combinatorics.KatonaCircle

NumberingdefMathlib.Combinatorics.KatonaCircle, type

Wording

numbering of X (from the name)

English

Let $X$ be a set. Then a numbering of $X$ is an element of the function that maps $X$ to the set of equivalences from $X$ to $\mathrm{Fin}$ applied to the cardinality of $X$.

Numbering.IsPrefixdefMathlib.Combinatorics.KatonaCircle, predicate

Wording

no wording

English

Let $f$ be a numbering of $X$. Let $s$ be a finite set of $X$. Then $\operatorname{IsPrefix}$ holds for $f$ and $s$, if for all elements $x_{1}$ of $X$, $x_{1}$ is an element of $s$, if and only if $\operatorname{val} (f (x_{1}))< \FinsetcardMACRoM {s}$.

Numbering.prefixeddefMathlib.Combinatorics.KatonaCircle, function or constant

Wording

no wording

English

Let $s$ be a finite set of $X$. Then $\operatorname{prefixed}$ applied to $s$ is a finite set of the set of numberings of $X$ defined as $\FinsetFilter {f}{\operatorname{IsPrefix} (f , s)}{\FinsetunivMACRoAC}$.

Numbering.prefixedEquivdefMathlib.Combinatorics.KatonaCircle, function or constant

Wording

no wording

English

Let $s$ be a finite set of $X$. Then $\operatorname{prefixedEquiv}$ applied to $s$ is an element of $\EquivMACRoAE {(\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {\operatorname{prefixed} (s)}{x_{2}})})}{\mathrm{Prod} (\mathrm{Numbering} (\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {s}{x_{3}})}), \mathrm{Numbering} (\SubtypeSet {x_{4}}{(\MembershipmemMACRoT {\operatorname{compl} (s)}{x_{4}})}))}$.

Mathlib.Combinatorics.Matroid.Basic

MatroidstructureMathlib.Combinatorics.Matroid.Basic, type

Wording

matroid of x (from the name)

English

Let $x$ be a set. Then the matroids of $x$ are a basic type.

Matroid.DepdefMathlib.Combinatorics.Matroid.Basic, predicate

Wording

no wording

English

Let $M$ be a matroid of $x$. Let $D$ be an element of $\wp x$. Then $\operatorname{Dep}$ holds for $M$ and $D$, if $M$ is not independent to $D$ and $D \leq \operatorname{E} (M)$.

Matroid.EdefMathlib.Combinatorics.Matroid.Basic, function or constant

Wording

no wording

English

Let $\mathrm{self}$ be a matroid of $x$. Then $\operatorname{E}$ applied to $\mathrm{self}$ is an element of $\wp x$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.

Matroid.ExchangePropertydefMathlib.Combinatorics.Matroid.Basic, predicate

Wording

P is a exchange property (from the name)

English

Let $P$ be a function from elements of $\wp x$ to propositions. Then $P$ is an exchange property, if for all elements $X$ and $Y$ of $\wp x$, if $P$ holds for $X$, then if $P$ holds for $Y$, then for all elements $a$ of $x$, if $\MembershipmemMACRoT {\operatorname{sdiff} (X , Y)}{a}$, then there exists an element $b$ of $x$, such that $\MembershipmemMACRoT {\operatorname{sdiff} (Y , X)}{b}$ and $P$ holds for $\operatorname{insert}$ applied to $b$ and $\operatorname{sdiff}$ applied to $X$ and $\operatorname{singleton}$ applied to $a$.

Matroid.ExistsMaximalSubsetPropertydefMathlib.Combinatorics.Matroid.Basic, predicate

Wording

no wording

English

Let $P$ be a function from elements of $\wp x$ to propositions. Let $X$ be an element of $\wp x$. Then $\operatorname{ExistsMaximalSubsetProperty}$ holds for $P$ and $X$, if for all elements $I$ of $\wp x$, if $P$ holds for $I$, then if $I \leq X$, then there exists an element $J$ of $\wp x$, such that $I \leq J$ and $J$ is maximal with respect to the function that maps $K$ to the proposition that $P$ holds for $K$ and $K \leq X$.

Matroid.FinitaryclassMathlib.Combinatorics.Matroid.Basic, predicate

Wording

M is finitary (from the name)

English

Let $M$ be a matroid of $x$. Then we can say that $M$ is finitary.

Matroid.FiniteclassMathlib.Combinatorics.Matroid.Basic, predicate

Wording

M is finite (from the name)

English

Let $M$ be a matroid of $x$. Then we can say that $M$ is finite.

Matroid.IndepdefMathlib.Combinatorics.Matroid.Basic, predicate

Wording

self is independent to x1 (from the name)

English

Let $\mathrm{self}$ be a matroid of $x$. Let $x_{1}$ be an element of $\wp x$. Then $\mathrm{self}$ is independent to $x_{1}$, if $\operatorname{proj2}$ holds for $\mathrm{self}$ and $x_{1}$.

Matroid.IsBasedefMathlib.Combinatorics.Matroid.Basic, predicate

Wording

no wording

English

Let $\mathrm{self}$ be a matroid of $x$. Let $x_{1}$ be an element of $\wp x$. Then $\operatorname{IsBase}$ holds for $\mathrm{self}$ and $x_{1}$, if $\operatorname{proj1}$ holds for $\mathrm{self}$ and $x_{1}$.

Matroid.IsBasisdefMathlib.Combinatorics.Matroid.Basic, predicate

Wording

no wording

English

Let $M$ be a matroid of $x$. Let $I$ and $X$ be elements of $\wp x$. Then $\operatorname{IsBasis}$ holds for $M$, $I$ and $X$, if $I$ is maximal with respect to the function that maps $A$ to the proposition that $M$ is independent to $A$ and $A \leq X$ and $X \leq \operatorname{E} (M)$.

Matroid.IsBasis'defMathlib.Combinatorics.Matroid.Basic, predicate

Wording

no wording

English

Let $M$ be a matroid of $x$. Let $I$ and $X$ be elements of $\wp x$. Then $\operatorname{IsBasis'}$ holds for $M$, $I$ and $X$, if $I$ is maximal with respect to the function that maps $A$ to the proposition that $M$ is independent to $A$ and $A \leq X$.

Matroid.NonemptyclassMathlib.Combinatorics.Matroid.Basic, predicate

Wording

M is nonempty (from the name)

English

Let $M$ be a matroid of $x$. Then we can say that $M$ is nonempty.

Matroid.RankFiniteclassMathlib.Combinatorics.Matroid.Basic, predicate

Wording

no wording

English

Let $M$ be a matroid of $x$. Then we can say that $\operatorname{RankFinite}$ holds for $M$.

Matroid.RankInfiniteclassMathlib.Combinatorics.Matroid.Basic, predicate

Wording

no wording

English

Let $M$ be a matroid of $x$. Then we can say that $\operatorname{RankInfinite}$ holds for $M$.

Matroid.RankPosclassMathlib.Combinatorics.Matroid.Basic, predicate

Wording

M is a rank positive part (from the name)

English

Let $M$ be a matroid of $x$. Then we can say that $M$ is a rank positive part.

Matroid.aesop_matdefMathlib.Combinatorics.Matroid.Basic, function or constant

Wording

no wording

English

generation took over the time limit

Matroid.copydefMathlib.Combinatorics.Matroid.Basic, function or constant

Wording

the copy of IsBase and Indep (from the name)

English

Let $M$ be a matroid of $x$. Let $E$ be an element of $\wp x$. Let $\mathrm{IsBase}$ and $\mathrm{Indep}$ be functions from elements of $\wp x$ to propositions. Assume that $\EqtMACRoH {E}{\operatorname{E} (M)}$. Assume that for all elements $B$ of $\wp x$, $\mathrm{IsBase}$ holds for $B$, if and only if $\operatorname{IsBase}$ holds for $M$ and $B$. Assume that for all elements $I$ of $\wp x$, $\mathrm{Indep}$ holds for $I$, if and only if $M$ is independent to $I$. Then the copy of $\mathrm{IsBase}$ and $\mathrm{Indep}$ is a matroid of $x$.

Matroid.copyBasedefMathlib.Combinatorics.Matroid.Basic, function or constant

Wording

the copy base of E and IsBase (from the name)

English

Let $M$ be a matroid of $x$. Let $E$ be an element of $\wp x$. Let $\mathrm{IsBase}$ be a function from elements of $\wp x$ to propositions. Assume that $\EqtMACRoH {E}{\operatorname{E} (M)}$. Assume that for all elements $B$ of $\wp x$, $\mathrm{IsBase}$ holds for $B$, if and only if $\operatorname{IsBase}$ holds for $M$ and $B$. Then the copy base of $E$ and $\mathrm{IsBase}$ is a matroid of $x$.

Matroid.copyIndepdefMathlib.Combinatorics.Matroid.Basic, function or constant

Wording

no wording

English

Let $M$ be a matroid of $x$. Let $E$ be an element of $\wp x$. Let $\mathrm{Indep}$ be a function from elements of $\wp x$ to propositions. Assume that $\EqtMACRoH {E}{\operatorname{E} (M)}$. Assume that for all elements $I$ of $\wp x$, $\mathrm{Indep}$ holds for $I$, if and only if $M$ is independent to $I$. Then $\operatorname{copyIndep}$ applied to $M$, $E$, $\mathrm{Indep}$, $\mathrm{hE}$ and $h$ is a matroid of $x$.

Mathlib.Combinatorics.Matroid.Circuit

Matroid.IsCircuitdefMathlib.Combinatorics.Matroid.Circuit, predicate

Wording

no wording

English

Let $M$ be a matroid of $x$. Let $x_{1}$ be an element of $\wp x$. Then $\operatorname{IsCircuit}$ holds for $M$ and $x_{1}$, if $x_{1}$ is minimal with respect to $\operatorname{Dep}$ applied to $M$.

Matroid.IsCocircuitdefMathlib.Combinatorics.Matroid.Circuit, predicate

Wording

no wording

English

Let $M$ be a matroid of $x$. Let $K$ be an element of $\wp x$. Then $\operatorname{IsCocircuit}$ holds for $M$ and $K$, if $\operatorname{IsCircuit}$ holds for the dual of $M$ and $K$.

Matroid.fundCircuitdefMathlib.Combinatorics.Matroid.Circuit, function or constant

Wording

no wording

English

Let $M$ be a matroid of $x$. Let $e$ be an element of $x$. Let $I$ be an element of $\wp x$. Then $\operatorname{fundCircuit}$ applied to $M$, $e$ and $I$ is an element of $\wp x$ defined as $\operatorname{insert}$ applied to $e$ and $\operatorname{inter}$ applied to $I$ and the intersection of $\operatorname{ofPred}$ applied to the function that maps $J$ to the proposition that $J \leq I$ and the closure of $M$ and $\operatorname{singleton}$ applied to $e$ is less than or equal to the closure of $M$ and $J$.

Matroid.fundCocircuitdefMathlib.Combinatorics.Matroid.Circuit, function or constant

Wording

no wording

English

Let $M$ be a matroid of $x$. Let $e$ be an element of $x$. Let $B$ be an element of $\wp x$. Then $\operatorname{fundCocircuit}$ applied to $M$, $e$ and $B$ is an element of $\wp x$ defined as $\operatorname{fundCircuit}$ applied to the dual of $M$, $e$ and $\operatorname{sdiff}$ applied to $\operatorname{E}$ applied to the dual of $M$ and $B$.

Mathlib.Combinatorics.Matroid.Closure

Matroid.IsFlatstructureMathlib.Combinatorics.Matroid.Closure, predicate

Wording

M is flat (from the docstring)

English

Let $M$ be a matroid of $x$. Let $F$ be an element of $\wp x$. Then we can say that $M$ is flat.

Matroid.SpanningstructureMathlib.Combinatorics.Matroid.Closure, predicate

Wording

no wording

English

Let $M$ be a matroid of $x$. Let $S$ be an element of $\wp x$. Then we can say that $\operatorname{Spanning}$ holds for $M$ and $S$.

Matroid.closuredefMathlib.Combinatorics.Matroid.Closure, function or constant

Wording

the closure of M and X (from the name)

English

Let $M$ be a matroid of $x$. Let $X$ be an element of $\wp x$. Then the closure of $M$ and $X$ is an element of $\wp x$ defined as the intersection of $\operatorname{ofPred}$ applied to the function that maps $F$ to the proposition that $M$ is flat and $\operatorname{inter} (X , \operatorname{E} (M))\leq F$.

Matroid.subtypeClosuredefMathlib.Combinatorics.Matroid.Closure, function or constant

Wording

the subtype closure of M (from the name)

English

Let $M$ be a matroid of $x$. Then the subtype closure of $M$ is a closure operator of the set of elements of $\operatorname{Iic}$ applied to $\operatorname{E}$ applied to $M$.

Mathlib.Combinatorics.Matroid.Constructions

Matroid.emptyOndefMathlib.Combinatorics.Matroid.Constructions, function or constant

Wording

no wording

English

Let $x$ be a set. Then $\operatorname{emptyOn}$ applied to $x$ is a matroid of $x$.

Matroid.freeOndefMathlib.Combinatorics.Matroid.Constructions, function or constant

Wording

no wording

English

Let $E$ be an element of $\wp x$. Then $\operatorname{freeOn}$ applied to $E$ is a matroid of $x$ defined as the dual of $\operatorname{loopyOn}$ applied to $E$.

Matroid.loopyOndefMathlib.Combinatorics.Matroid.Constructions, function or constant

Wording

no wording

English

Let $E$ be an element of $\wp x$. Then $\operatorname{loopyOn}$ applied to $E$ is a matroid of $x$ defined as $\operatorname{restrict}$ applied to $\operatorname{emptyOn}$ applied to $x$ and $E$.

Matroid.uniqueBaseOndefMathlib.Combinatorics.Matroid.Constructions, function or constant

Wording

no wording

English

Let $I$ and $E$ be elements of $\wp x$. Then $\operatorname{uniqueBaseOn}$ applied to $I$ and $E$ is a matroid of $x$ defined as $\operatorname{restrict}$ applied to $\operatorname{freeOn}$ applied to $I$ and $E$.

Mathlib.Combinatorics.Matroid.Dual

Matroid.CoindepdefMathlib.Combinatorics.Matroid.Dual, predicate

Wording

no wording

English

Let $M$ be a matroid of $x$. Let $I$ be an element of $\wp x$. Then $\operatorname{Coindep}$ holds for $M$ and $I$, if the dual of $M$ is independent to $I$.

Matroid.dualdefMathlib.Combinatorics.Matroid.Dual, function or constant

Wording

the dual of M (from the docstring)

English

Let $M$ be a matroid of $x$. Then the dual of $M$ is a matroid of $x$ defined as the matroid of the dual independent matroid of $M$.

Matroid.dualIndepMatroiddefMathlib.Combinatorics.Matroid.Dual, function or constant

Wording

the dual independent matroid of M (from the name)

English

Let $M$ be a matroid of $x$. Then the dual independent matroid of $M$ is an independent matroid of $x$.

Mathlib.Combinatorics.Matroid.IndepAxioms

IndepMatroidstructureMathlib.Combinatorics.Matroid.IndepAxioms, type

Wording

independent matroid of x (from the name)

English

Let $x$ be a set. Then the independent matroids of $x$ are a basic type.

IndepMatroid.EdefMathlib.Combinatorics.Matroid.IndepAxioms, function or constant

Wording

no wording

English

Let $\mathrm{self}$ be an independent matroid of $x$. Then $\operatorname{E}$ applied to $\mathrm{self}$ is an element of $\wp x$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.

IndepMatroid.IndepdefMathlib.Combinatorics.Matroid.IndepAxioms, predicate

Wording

self is independent to x1 (from the name)

English

Let $\mathrm{self}$ be an independent matroid of $x$. Let $x_{1}$ be an element of $\wp x$. Then $\mathrm{self}$ is independent to $x_{1}$, if $\operatorname{proj1}$ holds for $\mathrm{self}$ and $x_{1}$.

IndepMatroid.matroiddefMathlib.Combinatorics.Matroid.IndepAxioms, function or constant

Wording

the matroid of M (from the name)

English

Let $M$ be an independent matroid of $x$. Then the matroid of $M$ is a matroid of $x$.

IndepMatroid.ofBdddefMathlib.Combinatorics.Matroid.IndepAxioms, function or constant

Wording

the independent matroid of E and Indep (from the name)

English

Let $E$ be an element of $\wp x$. Let $\mathrm{Indep}$ be a function from elements of $\wp x$ to propositions such that $\mathrm{Indep}$ holds for $\operatorname{emptyCollection}$, for all elements $I_{3}$ of $\wp x$, for all elements $J$ of $\wp x$, if $\mathrm{Indep}$ holds for $J$, then if $I_{3} \leq J$, then $\mathrm{Indep}$ holds for $I_{3}$, for all elements $I_{2}$ of $\wp x$, for all elements $B$ of $\wp x$, if $\mathrm{Indep}$ holds for $I_{2}$, then if $I_{2}$ is not maximal with respect to $\mathrm{Indep}$, then if $B$ is maximal with respect to $\mathrm{Indep}$, then there exists an element $x_{1}$ of $x$ such that $\MembershipmemMACRoT {\operatorname{sdiff} (B , I_{2})}{x_{1}}$ and $\mathrm{Indep}$ holds for $\operatorname{insert}$ applied to $x_{1}$ and $I_{2}$, for all elements $I_{1}$ of $\wp x$, if $\mathrm{Indep}$ holds for $I_{1}$, then $I_{1} \leq E$ and there exists an element $n$ of $\Natural$ such that for all elements $I$ of $\wp x$, if $\mathrm{Indep}$ holds for $I$, then the cardinality in $I$ is less than or equal to $n$. Then the independent matroid of $E$ and $\mathrm{Indep}$ is an independent matroid of $x$ defined as $\operatorname{mk}$ applied to $E$, $\mathrm{Indep}$, $\mathrm{indep\_empty}$, $\mathrm{indep\_subset}$, $\mathrm{indep\_aug}$, the function that maps $X$ and $h$ to $\mathrm{Matroid\_\_existsMaximalSubsetProperty\_of\_bdd}$ applied to $\mathrm{indep\_bdd}$ and $X$ and $\mathrm{subset\_ground}$.

IndepMatroid.ofBddAugmentdefMathlib.Combinatorics.Matroid.IndepAxioms, function or constant

Wording

the independent matroid of E and Indep (from the name)

English

Let $E$ be an element of $\wp x$. Let $\mathrm{Indep}$ be a function from elements of $\wp x$ to propositions such that $\mathrm{Indep}$ holds for $\operatorname{emptyCollection}$, for all elements $I_{3}$ of $\wp x$, for all elements $J_{1}$ of the power set of $x$, if $\mathrm{Indep}$ holds for $J_{1}$, then if $I_{3} \leq J_{1}$, then $\mathrm{Indep}$ holds for $I_{3}$, for all elements $I_{2}$ of $\wp x$, for all elements $J$ of $\wp x$, if $\mathrm{Indep}$ holds for $I_{2}$, then if $\mathrm{Indep}$ holds for $J$, then if the cardinality in $I_{2}$ is less than the cardinality in $J$, then there exists an element $e$ of $x$ such that $e$ is an element of $J$, $e$ is not an element of $I_{2}$ and $\mathrm{Indep}$ holds for $\operatorname{insert}$ applied to $e$ and $I_{2}$, there exists a natural number $n$ such that for all elements $I_{1}$ of $\wp x$, if $\mathrm{Indep}$ holds for $I_{1}$, then the cardinality in $I_{1}$ is less than or equal to $n$ and for all elements $I$ of $\wp x$, if $\mathrm{Indep}$ holds for $I$, then $I \leq E$. Then the independent matroid of $E$ and $\mathrm{Indep}$ is an independent matroid of $x$.

IndepMatroid.ofFinitarydefMathlib.Combinatorics.Matroid.IndepAxioms, function or constant

Wording

the independent matroid of E and Indep (from the name)

English

Let $E$ be an element of $\wp x$. Let $\mathrm{Indep}$ be a function from elements of $\wp x$ to propositions such that $\mathrm{Indep}$ holds for $\operatorname{emptyCollection}$, for all elements $I_{3}$ of $\wp x$, for all elements $J_{1}$ of $\wp x$, if $\mathrm{Indep}$ holds for $J_{1}$, then if $I_{3} \leq J_{1}$, then $\mathrm{Indep}$ holds for $I_{3}$, for all elements $I_{2}$ of $\wp x$, for all elements $B$ of $\wp x$, if $\mathrm{Indep}$ holds for $I_{2}$, then if $I_{2}$ is not maximal with respect to $\mathrm{Indep}$, then if $B$ is maximal with respect to $\mathrm{Indep}$, then there exists an element $x_{1}$ of $x$ such that $\MembershipmemMACRoT {\operatorname{sdiff} (B , I_{2})}{x_{1}}$ and $\mathrm{Indep}$ holds for $\operatorname{insert}$ applied to $x_{1}$ and $I_{2}$, for all elements $I_{1}$ of $\wp x$, if for all elements $J$ of $\wp x$, if $J \leq I_{1}$, then if $J$ is finite, then $\mathrm{Indep}$ holds for $J$, then $\mathrm{Indep}$ holds for $I_{1}$ and for all elements $I$ of $\wp x$, if $\mathrm{Indep}$ holds for $I$, then $I \leq E$. Then the independent matroid of $E$ and $\mathrm{Indep}$ is an independent matroid of $x$.

IndepMatroid.ofFinitaryCardAugmentdefMathlib.Combinatorics.Matroid.IndepAxioms, function or constant

Wording

the independent matroid of E and Indep (from the name)

English

Let $E$ be an element of $\wp x$. Let $\mathrm{Indep}$ be a function from elements of $\wp x$ to propositions such that $\mathrm{Indep}$ holds for $\operatorname{emptyCollection}$, for all elements $I_{3}$ of $\wp x$, for all elements $J_{2}$ of $\wp x$, if $\mathrm{Indep}$ holds for $J_{2}$, then if $I_{3} \leq J_{2}$, then $\mathrm{Indep}$ holds for $I_{3}$, for all elements $I_{2}$ of $\wp x$, for all elements $J_{1}$ of $\wp x$, if $\mathrm{Indep}$ holds for $I_{2}$, then if $I_{2}$ is finite, then if $\mathrm{Indep}$ holds for $J_{1}$, then if $J_{1}$ is finite, then if the cardinality of $I_{2}$ is less than the cardinality of $J_{1}$, then there exists an element $e$ of $x$ such that $\MembershipmemMACRoT {J_{1}}{e}$, it is not the case that $\MembershipmemMACRoT {I_{2}}{e}$ and $\mathrm{Indep}$ holds for $\operatorname{insert}$ applied to $e$ and $I_{2}$, for all elements $I_{1}$ of $\wp x$, if for all elements $J$ of $\wp x$, if $J \leq I_{1}$, then if $J$ is finite, then $\mathrm{Indep}$ holds for $J$, then $\mathrm{Indep}$ holds for $I_{1}$ and for all elements $I$ of $\wp x$, if $\mathrm{Indep}$ holds for $I$, then $I \leq E$. Then the independent matroid of $E$ and $\mathrm{Indep}$ is an independent matroid of $x$.

IndepMatroid.ofFinitedefMathlib.Combinatorics.Matroid.IndepAxioms, function or constant

Wording

the independent matroid of Indep (from the name)

English

Assume that $E$ is finite. Let $\mathrm{Indep}$ be a function from elements of $\wp x$ to propositions such that $\mathrm{Indep}$ holds for $\operatorname{emptyCollection}$, for all elements $I_{2}$ of $\wp x$, for all elements $J_{1}$ of the power set of $x$, if $\mathrm{Indep}$ holds for $J_{1}$, then if $I_{2} \leq J_{1}$, then $\mathrm{Indep}$ holds for $I_{2}$, for all elements $I_{1}$ of $\wp x$, for all elements $J$ of $\wp x$, if $\mathrm{Indep}$ holds for $I_{1}$, then if $\mathrm{Indep}$ holds for $J$, then if the cardinality of $I_{1}$ is less than the cardinality of $J$, then there exists an element $e$ of $x$ such that $e$ is an element of $J$, $e$ is not an element of $I_{1}$ and $\mathrm{Indep}$ holds for $\operatorname{insert}$ applied to $e$ and $I_{1}$ and for all elements $I$ of $\wp x$, if $\mathrm{Indep}$ holds for $I$, then $I \leq E$. Then the independent matroid of $\mathrm{Indep}$ is an independent matroid of $x$.

IndepMatroid.ofFinsetdefMathlib.Combinatorics.Matroid.IndepAxioms, function or constant

Wording

the independent matroid of E and Indep (from the name)

English

Let $E$ be an element of $\wp x$. Let $\mathrm{Indep}$ be a function from finite sets of $x$ to propositions such that $\mathrm{Indep}$ holds for $\operatorname{emptyCollection}$, for all finite sets $I_{2}$ of $x$, for all finite sets $J_{1}$ of $x$, if $\mathrm{Indep}$ holds for $J_{1}$, then if $I_{2} \leq J_{1}$, then $\mathrm{Indep}$ holds for $I_{2}$, for all finite sets $I_{1}$ of $x$, for all finite sets $J$ of $x$, if $\mathrm{Indep}$ holds for $I_{1}$, then if $\mathrm{Indep}$ holds for $J$, then if $\FinsetcardMACRoM {I_{1}}< \FinsetcardMACRoM {J}$, then there exists an element $e$ of $x$ such that $e$ is an element of $J$, $e$ is not an element of $I_{1}$ and $\mathrm{Indep}$ holds for $\operatorname{insert}$ applied to $e$ and $I_{1}$ and for all finite sets $I$ of $x$, if $\mathrm{Indep}$ holds for $I$, then $I \leq E$. Then the independent matroid of $E$ and $\mathrm{Indep}$ is an independent matroid of $x$.

Matroid.ofBasedefMathlib.Combinatorics.Matroid.IndepAxioms, function or constant

Wording

the matroid of E and IsBase (from the name)

English

Let $E$ be an element of $\wp x$. Let $\mathrm{IsBase}$ be a function from elements of $\wp x$ to propositions such that there exists an element $B_{2}$ of $\wp x$ such that $\mathrm{IsBase}$ holds for $B_{2}$, $\mathrm{IsBase}$ is an exchange property, for all elements $X$ of $\wp x$, if $X \leq E$, then $\operatorname{ExistsMaximalSubsetProperty}$ holds for the function that maps $x_{1}$ to the proposition that there exists an element $B_{1}$ of $\wp x$ such that $\mathrm{IsBase}$ holds for $B_{1}$ and $x_{1} \leq B_{1}$ and $X$ and for all elements $B$ of $\wp x$, if $\mathrm{IsBase}$ holds for $B$, then $B \leq E$. Then the matroid of $E$ and $\mathrm{IsBase}$ is a matroid of $x$.

Matroid.ofExistsFiniteIsBasedefMathlib.Combinatorics.Matroid.IndepAxioms, function or constant

Wording

the matroid of E and IsBase (from the name)

English

Let $E$ be an element of $\wp x$. Let $\mathrm{IsBase}$ be a function from elements of $\wp x$ to propositions such that there exists an element $B_{1}$ of $\wp x$ such that $\mathrm{IsBase}$ holds for $B_{1}$ and $B_{1}$ is finite, $\mathrm{IsBase}$ is an exchange property and for all elements $B$ of $\wp x$, if $\mathrm{IsBase}$ holds for $B$, then $B \leq E$. Then the matroid of $E$ and $\mathrm{IsBase}$ is a matroid of $x$.

Matroid.ofExistsMatroiddefMathlib.Combinatorics.Matroid.IndepAxioms, function or constant

Wording

the matroid of E and Indep (from the name)

English

Let $E$ be an element of $\wp x$. Let $\mathrm{Indep}$ be a function from elements of $\wp x$ to propositions such that there exists a matroid $M$ of $x$, such that $\EqtMACRoH {E}{\operatorname{E} (M)}$ and for all elements $I$ of $\wp x$, $M$ is independent to $I$, if and only if $\mathrm{Indep}$ holds for $I$. Then the matroid of $E$ and $\mathrm{Indep}$ is a matroid of $x$.

Matroid.ofIsBaseOfFinitedefMathlib.Combinatorics.Matroid.IndepAxioms, function or constant

Wording

the matroid of IsBase (from the name)

English

Assume that $E$ is finite. Let $\mathrm{IsBase}$ be a function from elements of $\wp x$ to propositions such that there exists an element $B_{1}$ of $\wp x$ such that $\mathrm{IsBase}$ holds for $B_{1}$, $\mathrm{IsBase}$ is an exchange property and for all elements $B$ of $\wp x$, if $\mathrm{IsBase}$ holds for $B$, then $B \leq E$. Then the matroid of $\mathrm{IsBase}$ is a matroid of $x$.

Mathlib.Combinatorics.Matroid.Loop

Matroid.IsColoopdefMathlib.Combinatorics.Matroid.Loop, predicate

Wording

no wording

English

Let $M$ be a matroid of $x$. Let $e$ be an element of $x$. Then $\operatorname{IsColoop}$ holds for $M$ and $e$, if $\operatorname{IsLoop}$ holds for the dual of $M$ and $e$.

Matroid.IsLoopdefMathlib.Combinatorics.Matroid.Loop, predicate

Wording

no wording

English

Let $M$ be a matroid of $x$. Let $e$ be an element of $x$. Then $\operatorname{IsLoop}$ holds for $M$ and $e$, if $e$ is an element of the loop of $M$.

Matroid.IsNonloopstructureMathlib.Combinatorics.Matroid.Loop, predicate

Wording

no wording

English

Let $M$ be a matroid of $x$. Let $e$ be an element of $x$. Then we can say that $\operatorname{IsNonloop}$ holds for $M$ and $e$.

Matroid.LooplessclassMathlib.Combinatorics.Matroid.Loop, predicate

Wording

no wording

English

Let $M$ be a matroid of $x$. Then we can say that $\operatorname{Loopless}$ holds for $M$.

Matroid.coloopsdefMathlib.Combinatorics.Matroid.Loop, function or constant

Wording

no wording

English

Let $M$ be a matroid of $x$. Then $\operatorname{coloops}$ applied to $M$ is an element of $\wp x$ defined as the loop of the dual of $M$.

Matroid.loopsdefMathlib.Combinatorics.Matroid.Loop, function or constant

Wording

the loop of M (from the name)

English

Let $M$ be a matroid of $x$. Then the loop of $M$ is an element of $\wp x$ defined as the closure of $M$ and $\operatorname{emptyCollection}$.

Matroid.removeLoopsdefMathlib.Combinatorics.Matroid.Loop, function or constant

Wording

no wording

English

Let $M$ be a matroid of $x$. Then $\operatorname{removeLoops}$ applied to $M$ is a matroid of $x$ defined as $\operatorname{restrict}$ applied to $M$ and $\operatorname{ofPred}$ applied to the function that maps $e$ to $\operatorname{IsNonloop}$ applied to $M$ and $e$.

Mathlib.Combinatorics.Matroid.Map

Matroid.comapdefMathlib.Combinatorics.Matroid.Map, function or constant

Wording

the preimage of N and f (from the name)

English

Let $N$ be a matroid of $x_{1}$. Let $f$ be a function from elements of $x$ to elements of $x_{1}$. Then the preimage of $N$ and $f$ is a matroid of $x$.

Matroid.comapOndefMathlib.Combinatorics.Matroid.Map, function or constant

Wording

no wording

English

Let $N$ be a matroid of $x_{1}$. Let $E$ be an element of $\wp x$. Let $f$ be a function from elements of $x$ to elements of $x_{1}$. Then $\operatorname{comapOn}$ applied to $N$, $E$ and $f$ is a matroid of $x$ defined as $\operatorname{restrict}$ applied to the preimage of $N$ and $f$ and $E$.

Matroid.mapdefMathlib.Combinatorics.Matroid.Map, function or constant

Wording

the map of M and f (from the name)

English

Let $M$ be a matroid of $x$. Let $f$ be a function from elements of $x$ to elements of $x_{1}$ such that $f$ is injective on $\operatorname{E}$ applied to $M$. Then the map of $M$ and $f$ is a matroid of $x_{1}$.

Matroid.mapEmbeddingdefMathlib.Combinatorics.Matroid.Map, function or constant

Wording

the map embedding of M and f (from the name)

English

Let $M$ be a matroid of $x$. Let $f$ be an embedding of $x$ and $x_{1}$. Then the map embedding of $M$ and $f$ is a matroid of $x_{1}$.

Matroid.mapEquivdefMathlib.Combinatorics.Matroid.Map, function or constant

Wording

the map equivalence of M and f (from the name)

English

Let $M$ be a matroid of $x$. Let $f$ be an equivalence from $x$ to $x_{1}$. Then the map equivalence of $M$ and $f$ is a matroid of $x_{1}$ defined as the map embedding of $M$ and the embedding of $f$.

Matroid.mapSetEmbeddingdefMathlib.Combinatorics.Matroid.Map, function or constant

Wording

the map set embedding of M and f (from the name)

English

Let $M$ be a matroid of $x$. Let $f$ be an embedding of the set of elements of $\operatorname{E}$ applied to $M$ and $x_{1}$. Then the map set embedding of $M$ and $f$ is a matroid of $x_{1}$.

Matroid.mapSetEquivdefMathlib.Combinatorics.Matroid.Map, function or constant

Wording

the map set equivalence of M and e (from the name)

English

Let $M$ be a matroid of $x$. Let $e$ be an equivalence from the set of elements of $\operatorname{E}$ applied to $M$ to the set of elements of $E$. Then the map set equivalence of $M$ and $e$ is a matroid of $x_{1}$.

Matroid.restrictSubtypedefMathlib.Combinatorics.Matroid.Map, function or constant

Wording

no wording

English

Let $M$ be a matroid of $x$. Let $X$ be an element of $\wp x$. Then $\operatorname{restrictSubtype}$ applied to $M$ and $X$ is a matroid of the set of elements of $X$ defined as the preimage of $\operatorname{restrict}$ applied to $M$ and $X$ and the function that maps $x_{1}$ to $\MembershipmemMACRoT {X}{x_{1}}$.

Mathlib.Combinatorics.Matroid.Minor.Contract

Matroid.contractdefMathlib.Combinatorics.Matroid.Minor.Contract, function or constant

Wording

the contraction of M and C (from the docstring)

English

Let $M$ be a matroid of $x$. Let $C$ be an element of $\wp x$. Then the contraction of $M$ and $C$ is a matroid of $x$ defined as the dual of the deletion of the dual of $M$ and $C$.

Mathlib.Combinatorics.Matroid.Minor.Delete

Matroid.deletedefMathlib.Combinatorics.Matroid.Minor.Delete, function or constant

Wording

the deletion of M and D (from the docstring)

English

Let $M$ be a matroid of $x$. Let $D$ be an element of $\wp x$. Then the deletion of $M$ and $D$ is a matroid of $x$ defined as $\operatorname{restrict}$ applied to $M$ and $\operatorname{sdiff}$ applied to $\operatorname{E}$ applied to $M$ and $D$.

Mathlib.Combinatorics.Matroid.Minor.Order

Matroid.IsMinordefMathlib.Combinatorics.Matroid.Minor.Order, predicate

Wording

no wording

English

Let $N$ and $M$ be matroids of $x$. Then $\operatorname{IsMinor}$ holds for $N$ and $M$, if there exist elements $C$ and $D$ of $\wp x$, such that $N$ is equal to the deletion of the contraction of $M$ and $C$ and $D$.

Matroid.IsStrictMinordefMathlib.Combinatorics.Matroid.Minor.Order, predicate

Wording

no wording

English

Let $N$ and $M$ be matroids of $x$. Then $\operatorname{IsStrictMinor}$ holds for $N$ and $M$, if $\operatorname{IsMinor}$ holds for $N$ and $M$ and it is not the case that $\operatorname{IsMinor}$ holds for $M$ and $N$.

Mathlib.Combinatorics.Matroid.Minor.Restrict

Matroid.IsRestrictiondefMathlib.Combinatorics.Matroid.Minor.Restrict, predicate

Wording

no wording

English

Let $N$ and $M$ be matroids of $x$. Then $\operatorname{IsRestriction}$ holds for $N$ and $M$, if there exists an element $R$ of $\wp x$, such that $R \leq \operatorname{E} (M)$ and $\EqtMACRoH {N}{\operatorname{restrict} (M , R)}$.

Matroid.IsStrictRestrictiondefMathlib.Combinatorics.Matroid.Minor.Restrict, predicate

Wording

no wording

English

Let $N$ and $M$ be matroids of $x$. Then $\operatorname{IsStrictRestriction}$ holds for $N$ and $M$, if $\operatorname{IsRestriction}$ holds for $N$ and $M$ and it is not the case that $\operatorname{IsRestriction}$ holds for $M$ and $N$.

Matroid.MatroidᵣstructureMathlib.Combinatorics.Matroid.Minor.Restrict, type

Wording

matroid of x (from the name)

English

Let $x$ be a set. Then the matroids of $x$ are a basic type.

Matroid.Matroidᵣ.toMatroiddefMathlib.Combinatorics.Matroid.Minor.Restrict, function or constant

Wording

the matroid of self (from the name)

English

Let $\mathrm{self}$ be a matroid of $x$. Then the matroid of $\mathrm{self}$ is a matroid of $x$ defined as $\mathrm{Matroid\_\_Matroid\_u1d63\_\_\_proj0}$ applied to $\mathrm{self}$.

Matroid.restrictdefMathlib.Combinatorics.Matroid.Minor.Restrict, function or constant

Wording

no wording

English

Let $M$ be a matroid of $x$. Let $R$ be an element of $\wp x$. Then $\operatorname{restrict}$ applied to $M$ and $R$ is a matroid of $x$ defined as the matroid of $\operatorname{restrictIndepMatroid}$ applied to $M$ and $R$.

Matroid.restrictIndepMatroiddefMathlib.Combinatorics.Matroid.Minor.Restrict, function or constant

Wording

no wording

English

Let $M$ be a matroid of $x$. Let $R$ be an element of $\wp x$. Then $\operatorname{restrictIndepMatroid}$ applied to $M$ and $R$ is an independent matroid of $x$.

Mathlib.Combinatorics.Matroid.Rank.Cardinal

Matroid.InvariantCardinalRankclassMathlib.Combinatorics.Matroid.Rank.Cardinal, predicate

Wording

M is a invariant cardinal rank (from the name)

English

Let $M$ be a matroid of $x$. Then we can say that $M$ is an invariant cardinal rank.

Matroid.cRankdefMathlib.Combinatorics.Matroid.Rank.Cardinal, function or constant

Wording

the rank of M (from the name)

English

Let $M$ be a matroid of $x$. Then the rank of $M$ is a cardinal defined as the supremum of the function that maps $B$ to $\operatorname{mk}$ applied to the set of elements of $B$.

Matroid.cRkdefMathlib.Combinatorics.Matroid.Rank.Cardinal, function or constant

Wording

no wording

English

Let $M$ be a matroid of $x$. Let $X$ be an element of $\wp x$. Then $\operatorname{cRk}$ applied to $M$ and $X$ is a cardinal defined as the rank of $\operatorname{restrict}$ applied to $M$ and $X$.

Mathlib.Combinatorics.Matroid.Rank.ENat

Matroid.eRankdefMathlib.Combinatorics.Matroid.Rank.ENat, function or constant

Wording

the rank of M (from the docstring)

English

Let $M$ be a matroid of $x$. Then the rank of $M$ is a natural number defined as the supremum of the function that maps $B$ to the cardinality in $B$.

Matroid.eRkdefMathlib.Combinatorics.Matroid.Rank.ENat, function or constant

Wording

no wording

English

Let $M$ be a matroid of $x$. Let $X$ be an element of $\wp x$. Then $\operatorname{eRk}$ applied to $M$ and $X$ is a natural number defined as the rank of $\operatorname{restrict}$ applied to $M$ and $X$.

Mathlib.Combinatorics.Matroid.Rank.Finite

Matroid.IsRkFinitedefMathlib.Combinatorics.Matroid.Rank.Finite, predicate

Wording

no wording

English

Let $M$ be a matroid of $x$. Let $X$ be an element of $\wp x$. Then $\operatorname{IsRkFinite}$ holds for $M$ and $X$, if $\operatorname{RankFinite}$ holds for $\operatorname{restrict}$ applied to $M$ and $X$.

Mathlib.Combinatorics.Matroid.Sum

Matroid.disjointSigmadefMathlib.Combinatorics.Matroid.Sum, function or constant

Wording

the disjoint sigma of M and h (from the name)

English

Let $M$ be a function from elements of $x_{1}$ to matroids of $x$ such that $\operatorname{onFun}$ applied to the proposition that $\mathrm{Disjoint}$ and the function that maps $i$ to $\operatorname{E}$ applied to $M$ applied to $i$ is pairwise. Then the disjoint sigma of $M$ and $h$ is a matroid of $x$ defined as the map embedding of the sigma of the function that maps $i$ to $\operatorname{restrictSubtype}$ applied to $M$ applied to $i$ and $\operatorname{E}$ applied to $M$ applied to $i$ and the sigma set of $h$.

Matroid.disjointSumdefMathlib.Combinatorics.Matroid.Sum, function or constant

Wording

the disjoint sum of M and N (from the name)

English

Let $M$ and $N$ be matroids of $x$ such that $\operatorname{E}$ applied to $M$ is disjoint to $\operatorname{E}$ applied to $N$. Then the disjoint sum of $M$ and $N$ is a matroid of $x$ defined as the map embedding of the sum of $\operatorname{restrictSubtype}$ applied to $M$ and $\operatorname{E}$ applied to $M$ and $\operatorname{restrictSubtype}$ applied to $N$ and $\operatorname{E}$ applied to $N$ and the sum set of $h$.

Matroid.sigmadefMathlib.Combinatorics.Matroid.Sum, function or constant

Wording

the sigma of M (from the name)

English

Let $M$ be a function from elements $i_{1}$ of $x$ to matroids of $x_{1}$ applied to $i_{1}$. Then the sigma of $i_{1}$ is a matroid of $\Sigma$ applied to the function that maps $i$ to $x_{1}$ applied to $i$.

Matroid.sumdefMathlib.Combinatorics.Matroid.Sum, function or constant

Wording

the sum of M and N (from the name)

English

Let $M$ be a matroid of $x$. Let $N$ be a matroid of $x_{1}$. Then the sum of $M$ and $N$ is a matroid of $\mathrm{Sum}$ applied to $x$ and $x_{1}$.

Matroid.sum'defMathlib.Combinatorics.Matroid.Sum, function or constant

Wording

the sum of M (from the docstring)

English

Let $M$ be a function from elements of $x_{1}$ to matroids of $x$. Then the sum of $M$ is a matroid of $\mathrm{Prod}$ applied to $x_{1}$ and $x$ defined as the map equivalence of the sigma of $M$ and the sigma equivalence product of $x_{1}$ and $x$.

Mathlib.Combinatorics.Optimization.ValuedCSP

FractionalOperationdefMathlib.Combinatorics.Optimization.ValuedCSP, type

Wording

fractional operation of D and m (from the name)

English

Let $D$ be a set. Let $m$ be a natural number. Then a fractional operation of $D$ and $m$ is an element of the function that maps $D$ and $m$ to the set of multisets of the set of functions from functions from elements of $\mathrm{Fin}$ applied to $m$ to elements of $D$ to elements of $D$.

FractionalOperation.IsFractionalPolymorphismFordefMathlib.Combinatorics.Optimization.ValuedCSP, predicate

Wording

no wording

English

Let $x_{2}$ be a fractional operation of $D$ and $m$. Let $x_{3}$ be an element of $\mathrm{ValuedCSP}$ applied to $D$ and $C$. Then $\operatorname{IsFractionalPolymorphismFor}$ holds for $x_{2}$ and $x_{3}$, if for all elements $f$ of $\Sigma$ applied to the function that maps $n$ to the set of functions from functions from elements of $\mathrm{Fin}$ applied to $n$ to elements of $D$ to elements of $C$, if $f$ is an element of $x_{3}$, then $\operatorname{AdmitsFractional}$ holds for $\operatorname{snd}$ applied to $f$ and $x_{2}$.

FractionalOperation.IsSymmetricdefMathlib.Combinatorics.Optimization.ValuedCSP, predicate

Wording

x is symmetric (from the name)

English

Let $x$ be a fractional operation of $D$ and $m$. Then $x$ is symmetric, if for all functions $x_{1}$ and $y$ from elements of $\mathrm{Fin}$ applied to $m$ to elements of $D$, if $\operatorname{Perm}$ holds for $\operatorname{ofFn}$ applied to $x_{1}$ and $\operatorname{ofFn}$ applied to $y$, then for all functions $g$ from functions from elements of $\mathrm{Fin}$ applied to $m$ to elements of $D$ to elements of $D$, if $g$ is an element of $x$, then $\EqtMACRoH {g (x_{1})}{g (y)}$.

FractionalOperation.IsSymmetricFractionalPolymorphismFordefMathlib.Combinatorics.Optimization.ValuedCSP, predicate

Wording

no wording

English

Let $x_{2}$ be a fractional operation of $D$ and $m$. Let $x_{3}$ be an element of $\mathrm{ValuedCSP}$ applied to $D$ and $C$. Then $\operatorname{IsSymmetricFractionalPolymorphismFor}$ holds for $x_{2}$ and $x_{3}$, if $\operatorname{IsFractionalPolymorphismFor}$ holds for $x_{2}$ and $x_{3}$ and $x_{2}$ is symmetric.

FractionalOperation.IsValiddefMathlib.Combinatorics.Optimization.ValuedCSP, predicate

Wording

x is valid (from the name)

English

Let $x$ be a fractional operation of $D$ and $m$. Then $x$ is valid, if $x \neq \operatorname{emptyCollection}$.

FractionalOperation.sizedefMathlib.Combinatorics.Optimization.ValuedCSP, function or constant

Wording

no wording

English

Let $x$ be a fractional operation of $D$ and $m$. Then $\operatorname{size}$ applied to $x$ is a natural number defined as the cardinality of $x$.

FractionalOperation.ttdefMathlib.Combinatorics.Optimization.ValuedCSP, function or constant

Wording

no wording

English

Let $x_{1}$ be a fractional operation of $D$ and $m$. Let $x_{2}$ be a function from elements of $\mathrm{Fin}$ applied to $m$ and elements of $x$ to elements of $D$. Then $\operatorname{tt}$ applied to $x_{1}$ and $x_{2}$ is a multiset of the set of functions from elements of $x$ to elements of $D$ defined as the map of the function that maps $g$ and $i$ to $g$ applied to $\operatorname{swap}$ applied to $i$ and $x_{1}$.

Function.AdmitsFractionaldefMathlib.Combinatorics.Optimization.ValuedCSP, predicate

Wording

no wording

English

Let $f$ be a function from functions from elements of $\mathrm{Fin}$ applied to $n$ to elements of $D$ to elements of $C$. Let $x_{2}$ be a fractional operation of $D$ and $m$. Then $\operatorname{AdmitsFractional}$ holds for $f$ and $x_{2}$, if for all functions $x_{3}$ from elements of $\mathrm{Fin}$ applied to $m$ and elements of $\mathrm{Fin}$ applied to $n$ to elements of $D$, $\HSMulhSMulMACRoAL {m}{\operatorname{sum} (\operatorname{map} (f , \operatorname{tt} (x_{2} , x_{3})))}\leq \HSMulhSMulMACRoAL {\operatorname{size} (x_{2})}{(\FinsetSum {\FinsetunivMACRoAC}{i}{f (x_{3} (i))})}$.

Function.HasMaxCutPropertydefMathlib.Combinatorics.Optimization.ValuedCSP, predicate

Wording

f has a maximum cut property (from the name)

English

Let $f$ be a function from functions from elements of $\mathrm{Fin}$ applied to $2$ to elements of $D$ to elements of $C$. Then $f$ has a maximum cut property, if there exist elements $a$ and $b$ of $D$, such that $a \neq b$ and $\operatorname{HasMaxCutPropertyAt}$ holds for $f$, $a$ and $b$.

Function.HasMaxCutPropertyAtdefMathlib.Combinatorics.Optimization.ValuedCSP, predicate

Wording

no wording

English

Let $f$ be a function from functions from elements of $\mathrm{Fin}$ applied to $2$ to elements of $D$ to elements of $C$. Let $a$ and $b$ be elements of $D$. Then $\operatorname{HasMaxCutPropertyAt}$ holds for $f$, $a$ and $b$, if $\EqtMACRoH {f (\operatorname{vecCons} (a , \operatorname{vecCons} (b , \operatorname{vecEmpty})))}{f (\operatorname{vecCons} (b , \operatorname{vecCons} (a , \operatorname{vecEmpty})))}$ and for all elements $x_{1}$ of $D$, for all elements $y$ of $D$, $f (\operatorname{vecCons} (a , \operatorname{vecCons} (b , \operatorname{vecEmpty})))\leq f (\operatorname{vecCons} (x_{1} , \operatorname{vecCons} (y , \operatorname{vecEmpty})))$ and if $\EqtMACRoH {f (\operatorname{vecCons} (a , \operatorname{vecCons} (b , \operatorname{vecEmpty})))}{f (\operatorname{vecCons} (x_{1} , \operatorname{vecCons} (y , \operatorname{vecEmpty})))}$, then $\EqtMACRoH {a}{x_{1}}$ and $\EqtMACRoH {b}{y}$ or $\EqtMACRoH {a}{y}$ and $\EqtMACRoH {b}{x_{1}}$.

ValuedCSPdefMathlib.Combinatorics.Optimization.ValuedCSP, type

Wording

no wording

English

Let $D$ and $C$ be sets. Then an element of $\mathrm{ValuedCSP}$ applied to $D$ and $C$ is an element of the function that maps $D$ and $C$ to $\wp \Sigma (\lambda n . (\mathrm{Elem} (\mathrm{Fin} (n))\rightarrow D)\rightarrow C)$.

ValuedCSP.InstancedefMathlib.Combinatorics.Optimization.ValuedCSP, type

Wording

no wording

English

Let $x_{2}$ be an element of $\mathrm{ValuedCSP}$ applied to $D$ and $C$. Let $x_{3}$ be a set. Then an element of $\operatorname{Instance}$ applied to $x_{2}$ and $x_{3}$ is an element of the function that maps $x_{2}$ and $x_{3}$ to the set of multisets of the set of terms of $x_{2}$ and $x_{3}$.

ValuedCSP.Instance.IsOptimumSolutiondefMathlib.Combinatorics.Optimization.ValuedCSP, predicate

Wording

x4 is a optimum solution with respect to I (from the name)

English

Let $I$ be an element of $\operatorname{Instance}$ applied to $x_{2}$ and $x_{3}$. Let $x_{4}$ be a function from elements of $x_{3}$ to elements of $D$. Then $x_{4}$ is an optimum solution with respect to $I$, if for all functions $y$ from elements of $x_{3}$ to elements of $D$, the evaluation solution of $I$ and $x_{4}$ is less than or equal to the evaluation solution of $I$ and $y$.

ValuedCSP.Instance.evalSolutiondefMathlib.Combinatorics.Optimization.ValuedCSP, function or constant

Wording

the evaluation solution of I and x4 (from the name)

English

Let $I$ be an element of $\operatorname{Instance}$ applied to $x_{2}$ and $x_{3}$. Let $x_{4}$ be a function from elements of $x_{3}$ to elements of $D$. Then the evaluation solution of $I$ and $x_{4}$ is an element of $C$ defined as the sum of the map of the function that maps $x_{5}$ to the evaluation solution of $x_{5}$ and $x_{4}$ and $I$.

ValuedCSP.TermstructureMathlib.Combinatorics.Optimization.ValuedCSP, type

Wording

term of x2 and x3 (from the name)

English

Let $x_{2}$ be an element of $\mathrm{ValuedCSP}$ applied to $D$ and $C$. Let $x_{3}$ be a set. Then the terms of $x_{2}$ and $x_{3}$ are a basic type.

ValuedCSP.Term.appdefMathlib.Combinatorics.Optimization.ValuedCSP, function or constant

Wording

the term of self and x4 (from the name)

English

Let $\mathrm{self}$ be a term of $x_{2}$ and $x_{3}$. Let $x_{4}$ be an element of $\mathrm{Fin}$ applied to $\operatorname{n}$ applied to $\mathrm{self}$. Then the term of $\mathrm{self}$ and $x_{4}$ is an element of $x_{3}$ defined as $\operatorname{proj3}$ applied to $\mathrm{self}$ and $x_{4}$.

ValuedCSP.Term.evalSolutiondefMathlib.Combinatorics.Optimization.ValuedCSP, function or constant

Wording

the evaluation solution of t and x4 (from the name)

English

Let $t$ be a term of $x_{2}$ and $x_{3}$. Let $x_{4}$ be a function from elements of $x_{3}$ to elements of $D$. Then the evaluation solution of $t$ and $x_{4}$ is an element of $C$ defined as $\operatorname{f}$ applied to $t$ and $\operatorname{comp}$ applied to $x_{4}$ and $\operatorname{Term}$ applied to $t$.

ValuedCSP.Term.fdefMathlib.Combinatorics.Optimization.ValuedCSP, function or constant

Wording

no wording

English

Let $\mathrm{self}$ be a term of $x_{2}$ and $x_{3}$. Let $x_{4}$ be a function from elements of $\mathrm{Fin}$ applied to $\operatorname{n}$ applied to $\mathrm{self}$ to elements of $D$. Then $\operatorname{f}$ applied to $\mathrm{self}$ and $x_{4}$ is an element of $C$ defined as $\operatorname{proj1}$ applied to $\mathrm{self}$ and $x_{4}$.

ValuedCSP.Term.ndefMathlib.Combinatorics.Optimization.ValuedCSP, function or constant

Wording

no wording

English

Let $\mathrm{self}$ be a term of $x_{2}$ and $x_{3}$. Then $\operatorname{n}$ applied to $\mathrm{self}$ is a natural number defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.

Mathlib.Combinatorics.Quiver.Arborescence

Quiver.ArborescenceclassMathlib.Combinatorics.Quiver.Arborescence, predicate

Wording

V is a arborescence (from the name)

English

Let $V$ be a set. Then we can say that $V$ is an arborescence.

Quiver.Arborescence.rootdefMathlib.Combinatorics.Quiver.Arborescence, function or constant

Wording

the root of the arborescence (from the docstring)

English

The root of the arborescence is an element of $V$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.

Quiver.RootedConnectedclassMathlib.Combinatorics.Quiver.Arborescence, predicate

Wording

no wording

English

Let $r$ be an element of $V$. Then we can say that $\operatorname{RootedConnected}$ holds for $r$.

Quiver.geodesicSubtreedefMathlib.Combinatorics.Quiver.Arborescence, function or constant

Wording

the geodesic subtree of r (from the name)

English

Let $r$ be an element of $V$. Then the geodesic subtree of $r$ is a wide subquiver of $V$ defined as the function that maps $a$ and $b$ to $\operatorname{ofPred}$ applied to the function that maps $e$ to the proposition that there exists a path $p$ of $r$ and $a$, such that $\EqtMACRoH {\operatorname{shortestPath} (r , b)}{\operatorname{cons} (p , e)}$.

Quiver.rootdefMathlib.Combinatorics.Quiver.Arborescence, function or constant

Wording

the root of V (from the docstring)

English

Let $V$ be a set. Then the root of $V$ is an element of $V$ defined as the root of the arborescence.

Quiver.shortestPathdefMathlib.Combinatorics.Quiver.Arborescence, function or constant

Wording

no wording

English

Let $r$ and $b$ be elements of $V$. Then $\operatorname{shortestPath}$ applied to $r$ and $b$ is a path of $r$ and $b$.

Mathlib.Combinatorics.Quiver.Basic

QuiverclassMathlib.Combinatorics.Quiver.Basic, predicate

Wording

V is a quiver (from the name)

English

Let $V$ be a set. Then we can say that $V$ is a quiver.

Quiver.EmptydefMathlib.Combinatorics.Quiver.Basic, type

Wording

no wording

English

Let $V$ be a set. Then an element of $\operatorname{Empty}$ applied to $V$ is an element of the function that maps $V$ to $V$.

Quiver.HomdefMathlib.Combinatorics.Quiver.Basic, type

Wording

homomorphism of x and x1 (from the name)

English

Let $x$ and $x_{1}$ be elements of $V$. Then a homomorphism of $x$ and $x_{1}$ is an element of the function that maps $x$ and $x_{1}$ to $\operatorname{proj0}$ applied to $\mathrm{self}$, $x$ and $x_{1}$.

Quiver.Hom.opdefMathlib.Combinatorics.Quiver.Basic, function or constant

Wording

the opposite in f (from the docstring)

English

Let $f$ be a homomorphism of $X$ and $Y$. Then the opposite in $f$ is a homomorphism of $\operatorname{op}$ applied to $Y$ and $\operatorname{op}$ applied to $X$ defined as $\operatorname{op}$ applied to $f$.

Quiver.Hom.opEquivdefMathlib.Combinatorics.Quiver.Basic, function or constant

Wording

the opposite equivalence (from the name)

English

The opposite equivalence is an equivalence from the set of homomorphisms of $X$ and $Y$ to the set of homomorphisms of $\operatorname{op}$ applied to $Y$ and $\operatorname{op}$ applied to $X$.

Quiver.Hom.unopdefMathlib.Combinatorics.Quiver.Basic, function or constant

Wording

the opposite of f (from the name)

English

Let $f$ be a homomorphism of $X$ and $Y$. Then the opposite of $f$ is a homomorphism of the opposite of $Y$ and the opposite of $X$ defined as the opposite of $f$.

Quiver.IsThindefMathlib.Combinatorics.Quiver.Basic, predicate

Wording

V is thin (from the docstring)

English

Let $V$ be a set. Then $V$ is thin, if for all elements $a$ and $b$ of $V$, the set of homomorphisms of $a$ and $b$ is a subsingleton.

Quiver.homOfEqdefMathlib.Combinatorics.Quiver.Basic, function or constant

Wording

the homomorphism of f (from the name)

English

Let $f$ be a homomorphism of $X$ and $Y$. Assume that $\EqtMACRoH {X}{\mathrm{X'}}$. Assume that $\EqtMACRoH {Y}{\mathrm{Y'}}$. Then the homomorphism of $f$ is a homomorphism of $\mathrm{X'}$ and $\mathrm{Y'}$ defined as $\operatorname{ndrec}$ applied to $\operatorname{ndrec}$ applied to $f$ and $\mathrm{hY}$ and $\mathrm{hX}$.

Mathlib.Combinatorics.Quiver.Cast

Quiver.Hom.castdefMathlib.Combinatorics.Quiver.Cast, function or constant

Wording

the cast of e (from the name)

English

Assume that $\EqtMACRoH {u}{\mathrm{u'}}$. Assume that $\EqtMACRoH {v}{\mathrm{v'}}$. Let $e$ be a homomorphism of $u$ and $v$. Then the cast of $e$ is a homomorphism of $\mathrm{u'}$ and $\mathrm{v'}$ defined as $\operatorname{ndrec}$ applied to $\operatorname{ndrec}$ applied to $e$ and $\mathrm{hv}$ and $\mathrm{hu}$.

Quiver.Path.castdefMathlib.Combinatorics.Quiver.Cast, function or constant

Wording

the cast of p (from the name)

English

Assume that $\EqtMACRoH {u}{\mathrm{u'}}$. Assume that $\EqtMACRoH {v}{\mathrm{v'}}$. Let $p$ be a path of $u$ and $v$. Then the cast of $p$ is a path of $\mathrm{u'}$ and $\mathrm{v'}$ defined as $\operatorname{ndrec}$ applied to $\operatorname{ndrec}$ applied to $p$ and $\mathrm{hv}$ and $\mathrm{hu}$.

Mathlib.Combinatorics.Quiver.ConnectedComponent

Quiver.IsSStronglyConnecteddefMathlib.Combinatorics.Quiver.ConnectedComponent, predicate

Wording

V is strongly connected (from the name)

English

Let $V$ be a set. Then $V$ is strongly connected, if for all elements $i$ and $j$ of $V$, there exists a path $p$ of $i$ and $j$, such that $0$ is less than the length of $p$.

Quiver.IsStronglyConnecteddefMathlib.Combinatorics.Quiver.ConnectedComponent, predicate

Wording

V is strongly connected (from the name)

English

Let $V$ be a set. Then $V$ is strongly connected, if for all elements $i$ and $j$ of $V$, $\mathrm{Nonempty}$ holds for the set of paths of $i$ and $j$.

Quiver.StronglyConnectedComponentdefMathlib.Combinatorics.Quiver.ConnectedComponent, type

Wording

strongly connected component of V (from the name)

English

Let $V$ be a set. Then a strongly connected component of $V$ is an element of the function that maps $V$ to $\mathrm{Quotient}$ applied to $\operatorname{stronglyConnectedSetoid}$ applied to $V$.

Quiver.StronglyConnectedComponent.mkdefMathlib.Combinatorics.Quiver.ConnectedComponent, function or constant

Wording

no wording

English

Let $x_{1}$ be an element of $V$. Then $\operatorname{mk}$ applied to $x_{1}$ is a strongly connected component of $V$ defined as $\operatorname{mk'}$ applied to $x_{1}$.

Quiver.WeaklyConnectedComponentdefMathlib.Combinatorics.Quiver.ConnectedComponent, type

Wording

weakly connected component of V (from the name)

English

generation took over the time limit

Quiver.WeaklyConnectedComponent.mkdefMathlib.Combinatorics.Quiver.ConnectedComponent, function or constant

Wording

no wording

English

generation took over the time limit

Quiver.wideSubquiverSymmetrifydefMathlib.Combinatorics.Quiver.ConnectedComponent, function or constant

Wording

no wording

English

Let $H$ be a wide subquiver of $\operatorname{Symmetrify}$ applied to $V$. Then there is a wide subquiver of $V$. Proof. Let $H$ be arbitrary. Let $a$ be arbitrary. Let $b$ be arbitrary. Let $e$ be arbitrary. By a. By b. By H. By e. By Sum__inl. By Membership__mem. By b. By a. By H. By e. By Sum__inr. By Membership__mem. By or. By Set__ofPred.

Mathlib.Combinatorics.Quiver.Covering

Prefunctor.IsCoveringstructureMathlib.Combinatorics.Quiver.Covering, predicate

Wording

x2 is a covering (from the name)

English

Let $x_{2}$ be a prefunctor of $U$ and $V$. Then we can say that $x_{2}$ is a covering.

Prefunctor.costardefMathlib.Combinatorics.Quiver.Covering, function or constant

Wording

no wording

English

Let $x_{2}$ be a prefunctor of $U$ and $V$. Let $u$ be an element of $U$. Let $x_{3}$ be an element of $\operatorname{Costar}$ applied to $u$. Then $\operatorname{costar}$ applied to $x_{2}$, $u$ and $x_{3}$ is an element of $\operatorname{Costar}$ applied to the object of $x_{2}$ and $u$ defined as $\operatorname{mk}$ applied to the map of $x_{2}$ and $\operatorname{snd}$ applied to $x_{3}$.

Prefunctor.pathStardefMathlib.Combinatorics.Quiver.Covering, function or constant

Wording

the path star of u and x3 (from the name)

English

Let $x_{2}$ be a prefunctor of $U$ and $V$. Let $u$ be an element of $U$. Let $x_{3}$ be a path star of $u$. Then the path star of $u$ and $x_{3}$ is a path star of the object of $x_{2}$ and $u$ defined as $\operatorname{mk}$ applied to the image of $x_{2}$ and $\operatorname{snd}$ applied to $x_{3}$.

Prefunctor.stardefMathlib.Combinatorics.Quiver.Covering, function or constant

Wording

the star of u and x3 (from the name)

English

Let $x_{2}$ be a prefunctor of $U$ and $V$. Let $u$ be an element of $U$. Let $x_{3}$ be a star of $u$. Then the star of $u$ and $x_{3}$ is a star of the object of $x_{2}$ and $u$ defined as $\operatorname{mk}$ applied to the map of $x_{2}$ and $\operatorname{snd}$ applied to $x_{3}$.

Quiver.CostardefMathlib.Combinatorics.Quiver.Covering, type

Wording

no wording

English

Let $v$ be an element of $U$. Then an element of $\operatorname{Costar}$ applied to $v$ is an element of the function that maps $v$ to $\Sigma$ applied to the function that maps $u$ to the set of homomorphisms of $u$ and $v$.

Quiver.Costar.mkdefMathlib.Combinatorics.Quiver.Covering, function or constant

Wording

no wording

English

Let $f$ be a homomorphism of $u$ and $v$. Then $\operatorname{mk}$ applied to $f$ is an element of $\operatorname{Costar}$ applied to $v$ defined as $\operatorname{mk}$ applied to $u$ and $f$.

Quiver.PathStardefMathlib.Combinatorics.Quiver.Covering, type

Wording

path star of u (from the name)

English

Let $u$ be an element of $U$. Then a path star of $u$ is an element of the function that maps $u$ to $\Sigma$ applied to the function that maps $v$ to the set of paths of $u$ and $v$.

Quiver.PathStar.mkdefMathlib.Combinatorics.Quiver.Covering, function or constant

Wording

no wording

English

Let $p$ be a path of $u$ and $v$. Then $\operatorname{mk}$ applied to $p$ is a path star of $u$ defined as $\operatorname{mk}$ applied to $v$ and $p$.

Quiver.StardefMathlib.Combinatorics.Quiver.Covering, type

Wording

star of u (from the name)

English

Let $u$ be an element of $U$. Then a star of $u$ is an element of the function that maps $u$ to $\Sigma$ applied to the function that maps $v$ to the set of homomorphisms of $u$ and $v$.

Quiver.Star.mkdefMathlib.Combinatorics.Quiver.Covering, function or constant

Wording

no wording

English

Let $f$ be a homomorphism of $u$ and $v$. Then $\operatorname{mk}$ applied to $f$ is a star of $u$ defined as $\operatorname{mk}$ applied to $v$ and $f$.

Quiver.starEquivCostardefMathlib.Combinatorics.Quiver.Covering, function or constant

Wording

no wording

English

Let $u$ be an element of $U$. Then $\operatorname{starEquivCostar}$ applied to $u$ is an equivalence from the set of stars of $u$ to $\operatorname{Costar}$ applied to $u$.

Quiver.symmetrifyCostardefMathlib.Combinatorics.Quiver.Covering, function or constant

Wording

no wording

English

Let $u$ be an element of $U$. Then $\operatorname{symmetrifyCostar}$ applied to $u$ is an equivalence from $\operatorname{Costar}$ applied to the object of $\operatorname{of}$ and $u$ to $\mathrm{Sum}$ applied to $\operatorname{Costar}$ applied to $u$ and the set of stars of $u$ defined as $\operatorname{sigmaSumDistrib}$ applied to the function that maps $u_{1}$ to the set of homomorphisms of $u_{1}$ and the object of $\operatorname{of}$ and $u$ and the set of elements of $\operatorname{Hom}$ applied to the object of $\operatorname{of}$ and $u$.

Quiver.symmetrifyStardefMathlib.Combinatorics.Quiver.Covering, function or constant

Wording

the star of the symmetrification of u (from the docstring)

English

Let $u$ be an element of $U$. Then the star of the symmetrification of $u$ is an equivalence from the set of stars of the object of $\operatorname{of}$ and $u$ to $\mathrm{Sum}$ applied to the set of stars of $u$ and $\operatorname{Costar}$ applied to $u$ defined as $\operatorname{sigmaSumDistrib}$ applied to the set of elements of $\operatorname{Hom}$ applied to the object of $\operatorname{of}$ and $u$ and the function that maps $v$ to the set of homomorphisms of $v$ and the object of $\operatorname{of}$ and $u$.

Mathlib.Combinatorics.Quiver.Path

Prefunctor.mapPathdefMathlib.Combinatorics.Quiver.Path, function or constant

Wording

the image of F and x2 (from the docstring)

English

Let $F$ be a prefunctor of $V$ and $W$. Let $x_{2}$ be a path of $a$ and $b$. Then the image of $F$ and $x_{2}$ is a path of the object of $F$ and $a$ and the object of $F$ and $b$ defined as $\operatorname{brecOn}$ applied to $x_{2}$ and $\mathrm{Prefunctor\_\_mapPath\_\_\_f}$ applied to $F$.

Quiver.Hom.toPathdefMathlib.Combinatorics.Quiver.Path, function or constant

Wording

the path of e (from the name)

English

Let $e$ be a homomorphism of $a$ and $b$. Then the path of $e$ is a path of $a$ and $b$ defined as $\operatorname{cons}$ applied to $\operatorname{nil}$ and $e$.

Quiver.PathinductiveMathlib.Combinatorics.Quiver.Path, type

Wording

path of a and x1 (from the name)

English

Let $a$ and $x_{1}$ be elements of $V$. Then the paths of $a$ and $x_{1}$ are a basic type.

Quiver.Path.BoundedPathsdefMathlib.Combinatorics.Quiver.Path, type

Wording

bounded path of w and n (from the name)

English

Let $v$ and $w$ be elements of $V$. Let $n$ be an element of $\Natural$. Then a bounded path of $w$ and $n$ is an element of the function that maps $v$, $w$ and $n$ to $\SubtypeSet {p}{\mathrm{Leq} (\operatorname{length} (p), n)}$.

Quiver.Path.compdefMathlib.Combinatorics.Quiver.Path, function or constant

Wording

the composition of x1 and x2 (from the name)

English

Let $x_{1}$ be a path of $a$ and $b$. Let $x_{2}$ be a path of $b$ and $c$. Then the composition of $x_{1}$ and $x_{2}$ is a path of $a$ and $c$ defined as $\operatorname{brecOn}$ applied to $x_{2}$, $\mathrm{Quiver\_\_Path\_\_comp\_\_\_f}$ and $x_{1}$.

Quiver.Path.consconstructorMathlib.Combinatorics.Quiver.Path, function or constant

Wording

no wording

English

Let $x_{1}$ be a path of $a$ and $b$. Let $x_{2}$ be a homomorphism of $b$ and $c$. Then $\operatorname{cons}$ applied to $x_{1}$ and $x_{2}$ is a path of $a$ and $c$.

Quiver.Path.ctorElimTypedefMathlib.Combinatorics.Quiver.Path, type

Wording

no wording

English

Let $\mathrm{ctorIdx}$ be a natural number. Then an element of $\operatorname{ctorElimType}$ applied to $\mathrm{ctorIdx}$ is an element of the function that maps $\mathrm{ctorIdx}$ to $\mathrm{cond}$ applied to $\operatorname{ble}$ applied to $\mathrm{ctorIdx}$ and $0$, $\mathrm{PULift}$ applied to $\mathrm{motive}$ applied to $a$ and $\operatorname{nil}$ and $\mathrm{PULift}$ applied to the set of functions from elements $b$ of $V$ and elements $c$ of $V$ and paths $x_{1}$ of $a$ and $b$ and homomorphisms $x_{2}$ of $b$ and $c$ to elements of $\mathrm{motive}$ applied to $c$ and $\operatorname{cons}$ applied to $x_{1}$ and $x_{2}$.

Quiver.Path.lengthdefMathlib.Combinatorics.Quiver.Path, function or constant

Wording

the length of x1 (from the docstring)

English

Let $x_{1}$ be a path of $a$ and $b$. Then the length of $x_{1}$ is a natural number defined as $\operatorname{brecOn}$ applied to $x_{1}$ and $\mathrm{Quiver\_\_Path\_\_length\_\_\_f}$.

Quiver.Path.nilconstructorMathlib.Combinatorics.Quiver.Path, function or constant

Wording

no wording

English

$\operatorname{nil}$ is a path of $a$ and $a$.

Quiver.Path.toListdefMathlib.Combinatorics.Quiver.Path, function or constant

Wording

the list of x1 (from the name)

English

Let $x_{1}$ be a path of $a$ and $b$. Then the list of $x_{1}$ is a list of elements of $V$ defined as $\operatorname{brecOn}$ applied to $x_{1}$ and $\mathrm{Quiver\_\_Path\_\_toList\_\_\_f}$.

Quiver.ReachabledefMathlib.Combinatorics.Quiver.Path, predicate

Wording

no wording

English

Let $a$ and $b$ be elements of $V$. Then $\operatorname{Reachable}$ holds for $a$ and $b$, if $\mathrm{Nonempty}$ holds for the set of paths of $a$ and $b$.

Mathlib.Combinatorics.Quiver.Path.Vertices

Quiver.Path.enddefMathlib.Combinatorics.Quiver.Path.Vertices, function or constant

Wording

the end vertex of x1 (from the docstring)

English

Let $x_{1}$ be a path of $a$ and $b$. Then the end vertex of $x_{1}$ is an element of $V$.

Quiver.Path.verticesdefMathlib.Combinatorics.Quiver.Path.Vertices, function or constant

Wording

the vertice of x1 (from the name)

English

Let $x_{1}$ be a path of $a$ and $b$. Then the vertice of $x_{1}$ is a list of elements of $V$ defined as $\operatorname{brecOn}$ applied to $x_{1}$ and $\mathrm{Quiver\_\_Path\_\_vertices\_\_\_f}$.