Definitions: Mathlib.Combinatorics, part 3 of 3

156 definitions of 26 modules, Mathlib.Combinatorics.SimpleGraph.Regularity.Equitabilise to Mathlib.Combinatorics.Young.YoungDiagram. ‹ previous next ›

Mathlib.Combinatorics.SimpleGraph.Regularity.Equitabilise

Finpartition.equitabilisedefMathlib.Combinatorics.SimpleGraph.Regularity.Equitabilise, function or constant
Wording
no wording
English
Assume that $a \times m + b \times (m + 1)= \FinsetcardMACRoM {s}$. Then $\operatorname{equitabilise}$ applied to $h$ is a finpartition of $s$ defined as $\operatorname{choose}$ applied to $\mathrm{Finpartition\_\_equitabilise\_aux}$ applied to $h$.

Mathlib.Combinatorics.SimpleGraph.Regularity.Increment

SzemerediRegularity.incrementdefMathlib.Combinatorics.SimpleGraph.Regularity.Increment, function or constant
Wording
the increment of G and x4 (from the name)
English
Assume that $P$ is an equipartition. Let $G$ be a simple graph of $x$. Let $x_{4}$ be a real number. Then the increment of $G$ and $x_{4}$ is a finpartition of the universal set defined as $\operatorname{bind}$ applied to $P$ and the function that maps $x_{5}$ to $\operatorname{chunk}$ applied to $\mathrm{hP}$, $G$ and $x_{4}$.

Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform

Finpartition.IsUniformdefMathlib.Combinatorics.SimpleGraph.Regularity.Uniform, predicate
Wording
no wording
English
Let $P$ be a finpartition of $A$. Let $G$ be a simple graph of $x$. Let $x_{6}$ be an element of $x_{1}$. Then $\operatorname{IsUniform}$ holds for $P$, $G$ and $x_{6}$, if $\FinsetcardMACRoM {\operatorname{nonUniforms} (P , G , x_{6})}$ is less than or equal to the product of the cardinality of the set of parts of $P$, the difference between the cardinality of the set of parts of $P$ and $1$ and $x_{6}$.
Finpartition.nonUniformsdefMathlib.Combinatorics.SimpleGraph.Regularity.Uniform, function or constant
Wording
no wording
English
Let $P$ be a finpartition of $A$. Let $G$ be a simple graph of $x$. Let $x_{6}$ be an element of $x_{1}$. Then $\operatorname{nonUniforms}$ applied to $P$, $G$ and $x_{6}$ is a finite set of $\mathrm{Prod}$ applied to the set of finite sets of $x$ and the set of finite sets of $x$.
Finpartition.nonuniformWitnessesdefMathlib.Combinatorics.SimpleGraph.Regularity.Uniform, function or constant
Wording
no wording
English
Let $P$ be a finpartition of $A$. Let $G$ be a simple graph of $x$. Let $x_{6}$ be an element of $x_{1}$. Let $s$ be a finite set of $x$. Then $\operatorname{nonuniformWitnesses}$ applied to $P$, $G$, $x_{6}$ and $s$ is a finite set of the set of finite sets of $x$ defined as the forward image of $\FinsetFilter {t}{\mathrm{and} (\mathrm{Neq} (s , t), \mathrm{not} (\operatorname{IsUniform} (G , x_{6} , s , t)))}{\operatorname{parts} (P)}$ under $\operatorname{nonuniformWitness}$ applied to $G$, $x_{6}$ and $s$.
Finpartition.sparsePairsdefMathlib.Combinatorics.SimpleGraph.Regularity.Uniform, function or constant
Wording
the sparse pair of G and x6 (from the name)
English
Let $P$ be a finpartition of $A$. Let $G$ be a simple graph of $x$. Let $x_{6}$ be an element of $x_{1}$. Then the sparse pair of $G$ and $x_{6}$ is a finite set of $\mathrm{Prod}$ applied to the set of finite sets of $x$ and the set of finite sets of $x$.
SimpleGraph.IsUniformdefMathlib.Combinatorics.SimpleGraph.Regularity.Uniform, predicate
Wording
no wording
English
Let $G$ be a simple graph of $x$. Let $x_{5}$ be an element of $x_{1}$. Let $s$ and $t$ be finite sets of $x$. Then $\operatorname{IsUniform}$ holds for $G$, $x_{5}$, $s$ and $t$, if for all finite sets $\mathrm{s'}$ of $x$, if $\mathrm{s'} \leq s$, then for all finite sets $\mathrm{t'}$ of $x$, if $\mathrm{t'} \leq t$, then if $\FinsetcardMACRoM {s}\times x_{5} \leq \FinsetcardMACRoM {\mathrm{s'}}$, then if $\FinsetcardMACRoM {t}\times x_{5} \leq \FinsetcardMACRoM {\mathrm{t'}}$, then the absolute value of the difference between $\operatorname{cast}$ applied to the edge density of $\mathrm{s'}$ and $\mathrm{t'}$ and $\operatorname{cast}$ applied to the edge density of $s$ and $t$ is less than $x_{5}$.
SimpleGraph.nonuniformWitnessdefMathlib.Combinatorics.SimpleGraph.Regularity.Uniform, function or constant
Wording
no wording
English
Let $G$ be a simple graph of $x$. Let $x_{5}$ be an element of $x_{1}$. Let $s$ and $t$ be finite sets of $x$. Then $\operatorname{nonuniformWitness}$ applied to $G$, $x_{5}$, $s$ and $t$ is a finite set of $x$ defined as $\iteMACRoG {\mathrm{WellOrderingRel} (s , t)}{\ProdfstMACRoZ {\operatorname{nonuniformWitnesses} (G , x_{5} , s , t)}}{\ProdsndMACRoAA {\operatorname{nonuniformWitnesses} (G , x_{5} , t , s)}}$.
SimpleGraph.nonuniformWitnessesdefMathlib.Combinatorics.SimpleGraph.Regularity.Uniform, function or constant
Wording
no wording
English
Let $G$ be a simple graph of $x$. Let $x_{5}$ be an element of $x_{1}$. Let $s$ and $t$ be finite sets of $x$. Then $\operatorname{nonuniformWitnesses}$ applied to $G$, $x_{5}$, $s$ and $t$ is an element of $\mathrm{Prod}$ applied to the set of finite sets of $x$ and the set of finite sets of $x$.
SimpleGraph.regularityReduceddefMathlib.Combinatorics.SimpleGraph.Regularity.Uniform, function or constant
Wording
no wording
English
Let $P$ be a finpartition of $A$. Let $G$ be a simple graph of $x$. Let $x_{6}$ and $x_{7}$ be elements of $x_{1}$. Then $\operatorname{regularityReduced}$ applied to $P$, $G$, $x_{6}$ and $x_{7}$ is a simple graph of $x$.

Mathlib.Combinatorics.SimpleGraph.Star

SimpleGraph.Coloring.starGraphBooldefMathlib.Combinatorics.SimpleGraph.Star, function or constant
Wording
the star graph bool of r (from the name)
English
Let $r$ be an element of $V$. Then the star graph bool of $r$ is a coloring of the star graph of $r$ and $\mathrm{Bool}$.
SimpleGraph.starGraphdefMathlib.Combinatorics.SimpleGraph.Star, function or constant
Wording
the star graph of r (from the name)
English
Let $r$ be an element of $V$. Then the star graph of $r$ is a simple graph of $V$ defined as $\operatorname{fromRel}$ applied to the function that maps $v$ and $x$ to $\EqtMACRoH {v}{r}$.

Mathlib.Combinatorics.SimpleGraph.StronglyRegular

SimpleGraph.IsSRGWithstructureMathlib.Combinatorics.SimpleGraph.StronglyRegular, predicate
Wording
no wording
English
Let $G$ be a simple graph of $V$. Let $n$, $k$, $x_{2}$ and $x_{3}$ be natural numbers. Then we can say that $\operatorname{IsSRGWith}$ holds for $G$, $n$, $k$, $x_{2}$ and $x_{3}$.

Mathlib.Combinatorics.SimpleGraph.Subgraph

SimpleGraph.Embedding.ofIsInduceddefMathlib.Combinatorics.SimpleGraph.Subgraph, function or constant
Wording
the canonical embedding of #1 and #2 (from the docstring)
English
Let $\mathrm{G'}$ be an induced subgraph of $G$. Then the canonical embedding of $\mathrm{G'}$ and $\mathrm{hG'}$ is an embedding of the coercion of $\mathrm{G'}$ and $G$.
SimpleGraph.SubgraphstructureMathlib.Combinatorics.SimpleGraph.Subgraph, type
Wording
subgraph of G (from the name)
English
Let $G$ be a simple graph of $V$. Then the subgraphs of $G$ are a basic type.
SimpleGraph.Subgraph.AdjdefMathlib.Combinatorics.SimpleGraph.Subgraph, predicate
Wording
no wording
English
Let $\mathrm{self}$ be a subgraph of $G$. Let $x$ and $x_{1}$ be elements of $V$. Then $\operatorname{Adj}$ holds for $\mathrm{self}$, $x$ and $x_{1}$, if $\operatorname{proj1}$ holds for $\mathrm{self}$, $x$ and $x_{1}$.
SimpleGraph.Subgraph.IsInduceddefMathlib.Combinatorics.SimpleGraph.Subgraph, predicate
Wording
#1 is induced (from the name)
English
Let $\mathrm{G'}$ be a subgraph of $G$. Then $\mathrm{G'}$ is induced, if for all elements $v$ of $V$, if $\MembershipmemMACRoT {\operatorname{verts} (\mathrm{G'})}{v}$, then for all elements $w$ of $V$, if $\MembershipmemMACRoT {\operatorname{verts} (\mathrm{G'})}{w}$, then if $\operatorname{Adj}$ holds for $G$, $v$ and $w$, then $\operatorname{Adj}$ holds for $\mathrm{G'}$, $v$ and $w$.
SimpleGraph.Subgraph.IsSpanningdefMathlib.Combinatorics.SimpleGraph.Subgraph, predicate
Wording
#1 is a spanning (from the name)
English
Let $\mathrm{G'}$ be a subgraph of $G$. Then $\mathrm{G'}$ is a spanning, if for all elements $v$ of $V$, $\MembershipmemMACRoT {\operatorname{verts} (\mathrm{G'})}{v}$.
SimpleGraph.Subgraph.botIsodefMathlib.Combinatorics.SimpleGraph.Subgraph, function or constant
Wording
the bottom isomorphism (from the name)
English
The bottom isomorphism is an isomorphism of the coercion of the bottom and the empty graph of $\mathrm{Empty}$.
SimpleGraph.Subgraph.coedefMathlib.Combinatorics.SimpleGraph.Subgraph, function or constant
Wording
the coercion of #1 (from the name)
English
Let $\mathrm{G'}$ be a subgraph of $G$. Then the coercion of $\mathrm{G'}$ is a simple graph of the set of elements of $\operatorname{verts}$ applied to $\mathrm{G'}$.
SimpleGraph.Subgraph.coeDeleteVertsIsodefMathlib.Combinatorics.SimpleGraph.Subgraph, function or constant
Wording
no wording
English
Let $s$ be an element of $\wp V$. Then $\operatorname{coeDeleteVertsIso}$ applied to $s$ is an isomorphism of the coercion of $\operatorname{deleteVerts}$ applied to $\mathrm{G'}$ and $s$ and $\operatorname{induce}$ applied to $\operatorname{ofPred}$ applied to the function that maps $v$ to the proposition that $v$ is not an element of $s$ and the coercion of $\mathrm{G'}$.
SimpleGraph.Subgraph.coeEmbeddingSpanningCoedefMathlib.Combinatorics.SimpleGraph.Subgraph, function or constant
Wording
the coercion embedding spanning coercion of #1 (from the name)
English
Let $\mathrm{G'}$ be a subgraph of $G$. Then the coercion embedding spanning coercion of $\mathrm{G'}$ is an embedding of the coercion of $\mathrm{G'}$ and the spanning coercion of $\mathrm{G'}$.
SimpleGraph.Subgraph.coeInduceIsodefMathlib.Combinatorics.SimpleGraph.Subgraph, function or constant
Wording
no wording
English
Let $s$ be an element of $\wp V$ such that $s \leq \operatorname{verts} (\mathrm{G'})$. Then $\operatorname{coeInduceIso}$ applied to $s$ and $h$ is an isomorphism of the coercion of the induced subgraph of $\mathrm{G'}$ and $s$ and $\operatorname{induce}$ applied to $\operatorname{ofPred}$ applied to the function that maps $v$ to $\MembershipmemMACRoT {s}{v}$ and the coercion of $\mathrm{G'}$.
SimpleGraph.Subgraph.coeNeighborSetEquivdefMathlib.Combinatorics.SimpleGraph.Subgraph, function or constant
Wording
the coercion neighbor set equivalence of v (from the name)
English
Let $v$ be an element of $\operatorname{verts}$ applied to $\mathrm{G'}$. Then the coercion neighbor set equivalence of $v$ is an equivalence from the set of elements of the neighbor set of the coercion of $\mathrm{G'}$ and $v$ to the set of elements of the neighbor set of $\mathrm{G'}$ and $v$.
SimpleGraph.Subgraph.coeSubgraphdefMathlib.Combinatorics.SimpleGraph.Subgraph, function or constant
Wording
the coercion subgraph of x (from the name)
English
Let $x$ be a subgraph of the coercion of $\mathrm{G'}$. Then the coercion subgraph of $x$ is a subgraph of $G$ defined as the map of the homomorphism of $\mathrm{G'}$ and $x$.
SimpleGraph.Subgraph.comapdefMathlib.Combinatorics.SimpleGraph.Subgraph, function or constant
Wording
the preimage of f and H (from the name)
English
Let $f$ be a homomorphism of $G$ and $\mathrm{G'}$. Let $H$ be a subgraph of $\mathrm{G'}$. Then the preimage of $f$ and $H$ is a subgraph of $G$.
SimpleGraph.Subgraph.copydefMathlib.Combinatorics.SimpleGraph.Subgraph, function or constant
Wording
the copy of hadj and #4 (from the name)
English
Let $\mathrm{G'}$ be a subgraph of $G$. Let $\mathrm{V''}$ be an element of $\wp V$ such that $\EqtMACRoH {\mathrm{V''}}{\operatorname{verts} (\mathrm{G'})}$. Let $\mathrm{adj'}$ be a function from elements of $V$ and elements of $V$ to propositions such that $\EqtMACRoH {\mathrm{adj'}}{\operatorname{Adj} (\mathrm{G'})}$. Then the copy of $\mathrm{V''}$ and $\mathrm{adj'}$ is a subgraph of $G$.
SimpleGraph.Subgraph.degreedefMathlib.Combinatorics.SimpleGraph.Subgraph, function or constant
Wording
the degree of v and #2 (from the docstring)
English
Let $\mathrm{G'}$ be a subgraph of $G$. Let $v$ be an element of $V$. Then the degree of $\mathrm{G'}$ and $v$ is a natural number defined as the cardinality of the set of elements of the neighbor set of $\mathrm{G'}$ and $v$.
SimpleGraph.Subgraph.deleteEdgesdefMathlib.Combinatorics.SimpleGraph.Subgraph, function or constant
Wording
no wording
English
Let $\mathrm{G'}$ be a subgraph of $G$. Let $s$ be an element of the power set of the set of symmetric squares of $V$. Then $\operatorname{deleteEdges}$ applied to $\mathrm{G'}$ and $s$ is a subgraph of $G$.
SimpleGraph.Subgraph.deleteVertsdefMathlib.Combinatorics.SimpleGraph.Subgraph, function or constant
Wording
no wording
English
Let $\mathrm{G'}$ be a subgraph of $G$. Let $s$ be an element of $\wp V$. Then $\operatorname{deleteVerts}$ applied to $\mathrm{G'}$ and $s$ is a subgraph of $G$ defined as the induced subgraph of $\mathrm{G'}$ and $\operatorname{sdiff}$ applied to $\operatorname{verts}$ applied to $\mathrm{G'}$ and $s$.
SimpleGraph.Subgraph.edgeSetdefMathlib.Combinatorics.SimpleGraph.Subgraph, function or constant
Wording
the edge set of #1 (from the docstring)
English
Let $\mathrm{G'}$ be a subgraph of $G$. Then the edge set of $\mathrm{G'}$ is an element of the power set of the set of symmetric squares of $V$ defined as $\operatorname{fromRel}$ applied to $\operatorname{symm}$ applied to $\mathrm{G'}$.
SimpleGraph.Subgraph.homdefMathlib.Combinatorics.SimpleGraph.Subgraph, function or constant
Wording
the homomorphism of x (from the name)
English
Let $x$ be a subgraph of $G$. Then the homomorphism of $x$ is a homomorphism of the coercion of $x$ and $G$.
SimpleGraph.Subgraph.incidenceSetdefMathlib.Combinatorics.SimpleGraph.Subgraph, function or constant
Wording
the incidence set of v and #2 (from the name)
English
Let $\mathrm{G'}$ be a subgraph of $G$. Let $v$ be an element of $V$. Then the incidence set of $\mathrm{G'}$ and $v$ is an element of the power set of the set of symmetric squares of $V$ defined as $\operatorname{ofPred}$ applied to the function that maps $e$ to the proposition that $e$ is an element of the edge set of $\mathrm{G'}$ and $v$ is an element of $e$.
SimpleGraph.Subgraph.inclusiondefMathlib.Combinatorics.SimpleGraph.Subgraph, function or constant
Wording
the inclusion of h (from the name)
English
Assume that $x \leq y$. Then the inclusion of $h$ is a homomorphism of the coercion of $x$ and the coercion of $y$.
SimpleGraph.Subgraph.inducedefMathlib.Combinatorics.SimpleGraph.Subgraph, function or constant
Wording
the induced subgraph of s and #2 (from the docstring)
English
Let $\mathrm{G'}$ be a subgraph of $G$. Let $s$ be an element of $\wp V$. Then the induced subgraph of $\mathrm{G'}$ and $s$ is a subgraph of $G$.
SimpleGraph.Subgraph.mapdefMathlib.Combinatorics.SimpleGraph.Subgraph, function or constant
Wording
the map of f and H (from the name)
English
Let $f$ be a homomorphism of $G$ and $\mathrm{G'}$. Let $H$ be a subgraph of $G$. Then the map of $f$ and $H$ is a subgraph of $\mathrm{G'}$.
SimpleGraph.Subgraph.neighborSetdefMathlib.Combinatorics.SimpleGraph.Subgraph, function or constant
Wording
the neighbor set of v and #2 (from the name)
English
Let $\mathrm{G'}$ be a subgraph of $G$. Let $v$ be an element of $V$. Then the neighbor set of $\mathrm{G'}$ and $v$ is an element of $\wp V$ defined as $\operatorname{ofPred}$ applied to the function that maps $w$ to $\operatorname{Adj}$ applied to $\mathrm{G'}$, $v$ and $w$.
SimpleGraph.Subgraph.restrictdefMathlib.Combinatorics.SimpleGraph.Subgraph, function or constant
Wording
no wording
English
Let $x$ be a subgraph of $G$. Then $\operatorname{restrict}$ applied to $x$ is a subgraph of the coercion of $\mathrm{G'}$ defined as the preimage of the homomorphism of $\mathrm{G'}$ and $x$.
SimpleGraph.Subgraph.spanningCoedefMathlib.Combinatorics.SimpleGraph.Subgraph, function or constant
Wording
the spanning coercion of #1 (from the name)
English
Let $\mathrm{G'}$ be a subgraph of $G$. Then the spanning coercion of $\mathrm{G'}$ is a simple graph of $V$.
SimpleGraph.Subgraph.spanningCoeEquivCoeOfSpanningdefMathlib.Combinatorics.SimpleGraph.Subgraph, function or constant
Wording
the spanning coercion equivalence coercion of h and #2 (from the name)
English
Let $\mathrm{G'}$ be a subgraph of $G$ such that $\mathrm{G'}$ is a spanning. Then the spanning coercion equivalence coercion of $\mathrm{G'}$ and $h$ is an isomorphism of the spanning coercion of $\mathrm{G'}$ and the coercion of $\mathrm{G'}$.
SimpleGraph.Subgraph.spanningHomdefMathlib.Combinatorics.SimpleGraph.Subgraph, function or constant
Wording
the spanning homomorphism of x (from the name)
English
Let $x$ be a subgraph of $G$. Then the spanning homomorphism of $x$ is a homomorphism of the spanning coercion of $x$ and $G$ defined as $\operatorname{mk}$ applied to $\mathrm{id}$ and the function that maps $x_{1}$ and $x_{2}$ to $\mathrm{SimpleGraph\_\_Subgraph\_\_adj\_sub}$ applied to $x$.
SimpleGraph.Subgraph.supportdefMathlib.Combinatorics.SimpleGraph.Subgraph, function or constant
Wording
the support of H (from the name)
English
Let $H$ be a subgraph of $G$. Then the support of $H$ is an element of $\wp V$.
SimpleGraph.Subgraph.topIsodefMathlib.Combinatorics.SimpleGraph.Subgraph, function or constant
Wording
the top isomorphism (from the name)
English
The top isomorphism is an isomorphism of the coercion of the top and $G$.
SimpleGraph.Subgraph.vertdefMathlib.Combinatorics.SimpleGraph.Subgraph, function or constant
Wording
the vertex of v and h (from the name)
English
Let $\mathrm{G'}$ be a subgraph of $G$. Let $v$ be an element of $V$ such that $\MembershipmemMACRoT {\operatorname{verts} (\mathrm{G'})}{v}$. Then the vertex of $\mathrm{G'}$ and $v$ is an element of $\operatorname{verts}$ applied to $\mathrm{G'}$ defined as $v$.
SimpleGraph.Subgraph.vertsdefMathlib.Combinatorics.SimpleGraph.Subgraph, function or constant
Wording
no wording
English
Let $\mathrm{self}$ be a subgraph of $G$. Then $\operatorname{verts}$ applied to $\mathrm{self}$ is an element of $\wp V$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.
SimpleGraph.singletonSubgraphdefMathlib.Combinatorics.SimpleGraph.Subgraph, function or constant
Wording
the singleton subgraph of G and v (from the name)
English
Let $G$ be a simple graph of $V$. Let $v$ be an element of $V$. Then the singleton subgraph of $G$ and $v$ is a subgraph of $G$.
SimpleGraph.subgraphOfAdjdefMathlib.Combinatorics.SimpleGraph.Subgraph, function or constant
Wording
the subgraph of G and hvw (from the name)
English
Let $G$ be a simple graph of $V$ such that $\operatorname{Adj}$ holds for $G$, $v$ and $w$. Then the subgraph of $G$ and $\mathrm{hvw}$ is a subgraph of $G$.
SimpleGraph.toSubgraphdefMathlib.Combinatorics.SimpleGraph.Subgraph, function or constant
Wording
the subgraph of H and h (from the name)
English
Let $H$ be a simple graph of $V$ such that $H \leq G$. Then the subgraph of $H$ and $h$ is a subgraph of $G$ defined as $\operatorname{mk}$ applied to the universal set, $\operatorname{Adj}$ applied to $H$, the function that maps $x$, $x_{1}$ and $e$ to $h$ applied to $x$, $x_{1}$ and $e$, the function that maps $x_{2}$, $x_{3}$ and $h_{1}$ to $\mathrm{Set\_\_mem\_univ}$ applied to $x_{2}$ and $\operatorname{symm}$ applied to $H$.

Mathlib.Combinatorics.SimpleGraph.Sum

SimpleGraph.Coloring.sumdefMathlib.Combinatorics.SimpleGraph.Sum, function or constant
Wording
the sum of cG and cH (from the name)
English
Let $\mathrm{cG}$ be a coloring of $G$ and $x$. Let $\mathrm{cH}$ be a coloring of $H$ and $x$. Then the sum of $\mathrm{cG}$ and $\mathrm{cH}$ is a coloring of the sum of $G$ and $H$ and $x$.
SimpleGraph.Coloring.sumEquivdefMathlib.Combinatorics.SimpleGraph.Sum, function or constant
Wording
the sum equivalence (from the name)
English
The sum equivalence is an equivalence from the set of colorings of the sum of $G$ and $H$ and $x$ to $\mathrm{Prod}$ applied to the set of colorings of $G$ and $x$ and the set of colorings of $H$ and $x$.
SimpleGraph.Coloring.sumFindefMathlib.Combinatorics.SimpleGraph.Sum, function or constant
Wording
no wording
English
Let $\mathrm{cG}$ be a coloring of $G$ and $\mathrm{Fin}$ applied to $n$. Let $\mathrm{cH}$ be a coloring of $H$ and $\mathrm{Fin}$ applied to $m$. Then $\operatorname{sumFin}$ applied to $\mathrm{cG}$ and $\mathrm{cH}$ is a coloring of the sum of $G$ and $H$ and $\mathrm{Fin}$ applied to $\MaxmaxMACRoAF {n}{m}$ defined as the sum of $\operatorname{recolorOfEmbedding}$ applied to $G$, $\operatorname{castLEEmb}$ applied to $\mathrm{Nat\_\_le\_max\_left}$ applied to $n$ and $m$ and $\mathrm{cG}$ and $\operatorname{recolorOfEmbedding}$ applied to $H$, $\operatorname{castLEEmb}$ applied to $\mathrm{Nat\_\_le\_max\_right}$ applied to $n$ and $m$ and $\mathrm{cH}$.
SimpleGraph.Coloring.sumLeftdefMathlib.Combinatorics.SimpleGraph.Sum, function or constant
Wording
the left sum of c (from the name)
English
Let $c$ be a coloring of the sum of $G$ and $H$ and $x$. Then the left sum of $c$ is a coloring of $G$ and $x$ defined as the composition of $c$ and the homomorphism of the sum left injection.
SimpleGraph.Coloring.sumRightdefMathlib.Combinatorics.SimpleGraph.Sum, function or constant
Wording
the right sum of c (from the name)
English
Let $c$ be a coloring of the sum of $G$ and $H$ and $x$. Then the right sum of $c$ is a coloring of $H$ and $x$ defined as the composition of $c$ and the homomorphism of the sum right injection.
SimpleGraph.Embedding.sumdefMathlib.Combinatorics.SimpleGraph.Sum, function or constant
Wording
the sum of f and g (from the name)
English
Let $f$ be an embedding of $G$ and $\mathrm{G'}$. Let $g$ be an embedding of $H$ and $\mathrm{H'}$. Then the sum of $f$ and $g$ is an embedding of the sum of $G$ and $H$ and the sum of $\mathrm{G'}$ and $\mathrm{H'}$.
SimpleGraph.Embedding.sumInldefMathlib.Combinatorics.SimpleGraph.Sum, function or constant
Wording
the sum left injection (from the name)
English
The sum left injection is an embedding of $G$ and the sum of $G$ and $H$.
SimpleGraph.Embedding.sumInrdefMathlib.Combinatorics.SimpleGraph.Sum, function or constant
Wording
the sum right injection (from the name)
English
The sum right injection is an embedding of $H$ and the sum of $G$ and $H$.
SimpleGraph.Hom.sumdefMathlib.Combinatorics.SimpleGraph.Sum, function or constant
Wording
the sum of f and g (from the name)
English
Let $f$ be a homomorphism of $G$ and $\mathrm{G'}$. Let $g$ be a homomorphism of $H$ and $\mathrm{H'}$. Then the sum of $f$ and $g$ is a homomorphism of the sum of $G$ and $H$ and the sum of $\mathrm{G'}$ and $\mathrm{H'}$.
SimpleGraph.Iso.sumAssocdefMathlib.Combinatorics.SimpleGraph.Sum, function or constant
Wording
the disjoint sum (from the docstring)
English
The disjoint sum is an isomorphism of the sum of the sum of $G$ and $H$ and $I$ and the sum of $G$ and the sum of $H$ and $I$.
SimpleGraph.Iso.sumCommdefMathlib.Combinatorics.SimpleGraph.Sum, function or constant
Wording
the disjoint sum (from the docstring)
English
The disjoint sum is an isomorphism of the sum of $G$ and $H$ and the sum of $H$ and $G$.
SimpleGraph.Iso.sumCongrdefMathlib.Combinatorics.SimpleGraph.Sum, function or constant
Wording
the sum congruence of f and g (from the name)
English
Let $f$ be an isomorphism of $G$ and $\mathrm{G'}$. Let $g$ be an isomorphism of $H$ and $\mathrm{H'}$. Then the sum congruence of $f$ and $g$ is an isomorphism of the sum of $G$ and $H$ and the sum of $\mathrm{G'}$ and $\mathrm{H'}$.
SimpleGraph.edgeSetSumEquivdefMathlib.Combinatorics.SimpleGraph.Sum, function or constant
Wording
the edge set sum equivalence (from the name)
English
The edge set sum equivalence is an equivalence from the set of elements of the edge set for the sum of $G$ and $H$ to $\mathrm{Sum}$ applied to the set of elements of the edge set for $G$ and the set of elements of the edge set for $H$.
SimpleGraph.sumdefMathlib.Combinatorics.SimpleGraph.Sum, function or constant
Wording
the sum of G and H (from the name)
English
Let $G$ be a simple graph of $V$. Let $H$ be a simple graph of $W$. Then the sum of $G$ and $H$ is a simple graph of $\mathrm{Sum}$ applied to $V$ and $W$.

Mathlib.Combinatorics.SimpleGraph.Trails

SimpleGraph.Walk.IsEuleriandefMathlib.Combinatorics.SimpleGraph.Trails, predicate
Wording
no wording
English
Let $p$ be a walk of $u$ and $v$. Then $\operatorname{IsEulerian}$ holds for $p$, if for all symmetric squares $e$ of $V$, if $e$ is an element of the edge set for $G$, then the multiplicity of $e$ in the edge of $p$ is equal to $1$.
SimpleGraph.Walk.IsTrail.edgesFinsetdefMathlib.Combinatorics.SimpleGraph.Trails, function or constant
Wording
the edge finite set of h (from the name)
English
Assume that $p$ is a trail. Then the edge finite set of $h$ is a finite set of the set of symmetric squares of $V$.

Mathlib.Combinatorics.SimpleGraph.Triangle.Basic

SimpleGraph.EdgeDisjointTrianglesdefMathlib.Combinatorics.SimpleGraph.Triangle.Basic, predicate
Wording
no wording
English
Let $G$ be a simple graph of $x$. Then $\operatorname{EdgeDisjointTriangles}$ holds for $G$, if $\operatorname{Pairwise}$ holds for the clique set of $G$ and $3$ and the function that maps $x_{1}$ and $y$ to the proposition that $\operatorname{inter}$ applied to $x_{1}$ and $y$ is a subsingleton.
SimpleGraph.FarFromTriangleFreedefMathlib.Combinatorics.SimpleGraph.Triangle.Basic, predicate
Wording
no wording
English
Let $G$ be a simple graph of $x$. Let $x_{4}$ be an element of $x_{1}$. Then $\operatorname{FarFromTriangleFree}$ holds for $G$ and $x_{4}$, if $\operatorname{DeleteFar}$ holds for $G$, the function that maps $H$ to $\operatorname{CliqueFree}$ applied to $H$ and $3$ and the product of $x_{4}$ and the exponentiation of the cardinality of $x$ to $2$.
SimpleGraph.LocallyLineardefMathlib.Combinatorics.SimpleGraph.Triangle.Basic, predicate
Wording
G is locally linear (from the docstring)
English
generation took over the time limit

Mathlib.Combinatorics.SimpleGraph.Triangle.Removal

SimpleGraph.triangleRemovalBounddefMathlib.Combinatorics.SimpleGraph.Triangle.Removal, function or constant
Wording
no wording
English
Let $x$ be a real number. Then $\operatorname{triangleRemovalBound}$ applied to $x$ is a real number defined as the minimum of $\operatorname{inv}$ applied to $2 \times \operatorname{ceil} (\frac{ 4}{x})^ {3}$ and the product of $1 - \frac{ \MinminMACRoAG {1}{x}}{4}$ and the exponentiation of the quotient of $x$ and the product of $16$ and the bound of $\frac{ x}{8}$ and $\operatorname{ceil}$ applied to $\frac{ 4}{x}$ to $3$.

Mathlib.Combinatorics.SimpleGraph.Triangle.Tripartite

SimpleGraph.TripartiteFromTriangles.ExplicitDisjointclassMathlib.Combinatorics.SimpleGraph.Triangle.Tripartite, predicate
Wording
no wording
English
Let $t$ be a finite set of $\mathrm{Prod}$ applied to $x$ and $\mathrm{Prod}$ applied to $x_{1}$ and $x_{2}$. Then we can say that $\operatorname{ExplicitDisjoint}$ holds for $t$.
SimpleGraph.TripartiteFromTriangles.NoAccidentalclassMathlib.Combinatorics.SimpleGraph.Triangle.Tripartite, predicate
Wording
no wording
English
Let $t$ be a finite set of $\mathrm{Prod}$ applied to $x$ and $\mathrm{Prod}$ applied to $x_{1}$ and $x_{2}$. Then we can say that $\operatorname{NoAccidental}$ holds for $t$.
SimpleGraph.TripartiteFromTriangles.RelinductiveMathlib.Combinatorics.SimpleGraph.Triangle.Tripartite, predicate
Wording
no wording
English
Let $t$ be a finite set of $\mathrm{Prod}$ applied to $x$ and $\mathrm{Prod}$ applied to $x_{1}$ and $x_{2}$. Let $x_{3}$ and $x_{4}$ be elements of $\mathrm{Sum}$ applied to $x$ and $\mathrm{Sum}$ applied to $x_{1}$ and $x_{2}$. Then we can say that $\operatorname{Rel}$ holds for $t$, $x_{3}$ and $x_{4}$.
SimpleGraph.TripartiteFromTriangles.graphdefMathlib.Combinatorics.SimpleGraph.Triangle.Tripartite, function or constant
Wording
the graph of t (from the name)
English
Let $t$ be a finite set of $\mathrm{Prod}$ applied to $x$ and $\mathrm{Prod}$ applied to $x_{1}$ and $x_{2}$. Then the graph of $t$ is a simple graph of $\mathrm{Sum}$ applied to $x$ and $\mathrm{Sum}$ applied to $x_{1}$ and $x_{2}$.
SimpleGraph.TripartiteFromTriangles.toTriangledefMathlib.Combinatorics.SimpleGraph.Triangle.Tripartite, function or constant
Wording
the triangle (from the name)
English
The triangle is an embedding of $\mathrm{Prod}$ applied to $x$ and $\mathrm{Prod}$ applied to $x_{1}$ and $x_{2}$ and the set of finite sets of $\mathrm{Sum}$ applied to $x$ and $\mathrm{Sum}$ applied to $x_{1}$ and $x_{2}$.

Mathlib.Combinatorics.SimpleGraph.Tutte

SimpleGraph.IsTutteViolatordefMathlib.Combinatorics.SimpleGraph.Tutte, predicate
Wording
no wording
English
Let $G$ be a simple graph of $V$. Let $u$ be an element of $\wp V$. Then $\operatorname{IsTutteViolator}$ holds for $G$ and $u$, if the cardinality of $u$ is less than the cardinality of the odd component of the coercion of $\operatorname{deleteVerts}$ applied to the top and $u$.

Mathlib.Combinatorics.SimpleGraph.UnitDistance.Basic

SimpleGraph.UnitDistEmbeddingstructureMathlib.Combinatorics.SimpleGraph.UnitDistance.Basic, type
Wording
unit distance embedding of G and E (from the name)
English
Let $G$ be a simple graph of $V$. Let $E$ be a set. Then the unit distance embeddings of $G$ and $E$ are a basic type.
SimpleGraph.UnitDistEmbedding.botdefMathlib.Combinatorics.SimpleGraph.UnitDistance.Basic, function or constant
Wording
the bottom of p (from the name)
English
Let $p$ be an embedding of $V$ and $E$. Then the bottom of $p$ is a unit distance embedding of the bottom and $E$.
SimpleGraph.UnitDistEmbedding.copydefMathlib.Combinatorics.SimpleGraph.UnitDistance.Basic, function or constant
Wording
the copy of U and f (from the name)
English
Let $U$ be a unit distance embedding of $G$ and $E$. Let $f$ be a copy of $H$ and $G$. Then the copy of $U$ and $f$ is a unit distance embedding of $H$ and $E$.
SimpleGraph.UnitDistEmbedding.embeddefMathlib.Combinatorics.SimpleGraph.UnitDistance.Basic, function or constant
Wording
the embed of U and f (from the name)
English
Let $U$ be a unit distance embedding of $G$ and $E$. Let $f$ be an embedding of $H$ and $G$. Then the embed of $U$ and $f$ is a unit distance embedding of $H$ and $E$ defined as the copy of $U$ and the copy of $f$.
SimpleGraph.UnitDistEmbedding.isodefMathlib.Combinatorics.SimpleGraph.UnitDistance.Basic, function or constant
Wording
the isomorphism of U and e (from the name)
English
Let $U$ be a unit distance embedding of $G$ and $E$. Let $e$ be an isomorphism of $G$ and $H$. Then the isomorphism of $U$ and $e$ is a unit distance embedding of $H$ and $E$ defined as the copy of $U$ and the copy of the inverse of $e$.
SimpleGraph.UnitDistEmbedding.pdefMathlib.Combinatorics.SimpleGraph.UnitDistance.Basic, function or constant
Wording
no wording
English
Let $\mathrm{self}$ be a unit distance embedding of $G$ and $E$. Then $\operatorname{p}$ applied to $\mathrm{self}$ is an embedding of $V$ and $E$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.
SimpleGraph.UnitDistEmbedding.subsingletondefMathlib.Combinatorics.SimpleGraph.UnitDistance.Basic, function or constant
Wording
the subsingleton of G and x1 (from the name)
English
Let $G$ be a simple graph of $V$. Let $x_{1}$ be an element of $E$. Then the subsingleton of $G$ and $x_{1}$ is a unit distance embedding of $G$ and $E$.

Mathlib.Combinatorics.SimpleGraph.UniversalVerts

SimpleGraph.deleteUniversalVertsdefMathlib.Combinatorics.SimpleGraph.UniversalVerts, function or constant
Wording
no wording
English
Let $G$ be a simple graph of $V$. Then $\operatorname{deleteUniversalVerts}$ applied to $G$ is a subgraph of $G$ defined as $\operatorname{deleteVerts}$ applied to the top and $\operatorname{universalVerts}$ applied to $G$.
SimpleGraph.universalVertsdefMathlib.Combinatorics.SimpleGraph.UniversalVerts, function or constant
Wording
no wording
English
Let $G$ be a simple graph of $V$. Then $\operatorname{universalVerts}$ applied to $G$ is an element of $\wp V$ defined as $\operatorname{ofPred}$ applied to the function that maps $v$ to the proposition that $G$ is universal.

Mathlib.Combinatorics.SimpleGraph.VertexCover

SimpleGraph.IsVertexCoverdefMathlib.Combinatorics.SimpleGraph.VertexCover, predicate
Wording
no wording
English
Let $G$ be a simple graph of $V$. Let $c$ be an element of $\wp V$. Then $\operatorname{IsVertexCover}$ holds for $G$ and $c$, if for all elements $v$ and $w$ of $V$, if $\operatorname{Adj}$ holds for $G$, $v$ and $w$, then $v$ is an element of $c$ or $w$ is an element of $c$.
SimpleGraph.vertexCoverNumdefMathlib.Combinatorics.SimpleGraph.VertexCover, function or constant
Wording
the vertex cover number of G (from the docstring)
English
Let $G$ be a simple graph of $V$. Then the vertex cover number of $G$ is a natural number defined as the infimum of the function that maps $s$ to the infimum of the function that maps $h$ to the cardinality in $s$.

Mathlib.Combinatorics.SimpleGraph.Walk.Basic

SimpleGraph.Adj.toWalkdefMathlib.Combinatorics.SimpleGraph.Walk.Basic, function or constant
Wording
the walk of h (from the name)
English
Assume that $\operatorname{Adj}$ holds for $G$, $u$ and $v$. Then the walk of $h$ is a walk of $u$ and $v$ defined as $\operatorname{cons}$ applied to $h$ and $\operatorname{nil}$.
SimpleGraph.WalkinductiveMathlib.Combinatorics.SimpleGraph.Walk.Basic, type
Wording
walk of x and x1 (from the name)
English
Let $G$ be a simple graph of $V$. Let $x$ and $x_{1}$ be elements of $V$. Then the walks of $x$ and $x_{1}$ are a basic type.
SimpleGraph.Walk.NilinductiveMathlib.Combinatorics.SimpleGraph.Walk.Basic, predicate
Wording
no wording
English
Let $x$ be a walk of $v$ and $w$. Then we can say that $\operatorname{Nil}$ holds for $x$.
SimpleGraph.Walk.consconstructorMathlib.Combinatorics.SimpleGraph.Walk.Basic, function or constant
Wording
no wording
English
Assume that $\operatorname{Adj}$ holds for $G$, $u$ and $v$. Let $p$ be a walk of $v$ and $w$. Then $\operatorname{cons}$ applied to $h$ and $p$ is a walk of $u$ and $w$.
SimpleGraph.Walk.cons'defMathlib.Combinatorics.SimpleGraph.Walk.Basic, function or constant
Wording
no wording
English
Let $u$, $v$ and $w$ be elements of $V$ such that $\operatorname{Adj}$ holds for $G$, $u$ and $v$. Let $p$ be a walk of $v$ and $w$. Then $\operatorname{cons'}$ applied to $u$, $v$, $w$, $h$ and $p$ is a walk of $u$ and $w$ defined as $\operatorname{cons}$ applied to $h$ and $p$.
SimpleGraph.Walk.ctorElimTypedefMathlib.Combinatorics.SimpleGraph.Walk.Basic, 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 the set of functions from elements $u$ of $V$ to elements of $\mathrm{motive}$ applied to $u$, $u$ and $\operatorname{nil}$ and $\mathrm{PULift}$ applied to the set of functions from elements $u_{1}$ of $V$ and elements $v$ of $V$ and elements $w$ of $V$ and elements $h$ of $\mathrm{Proof}$ applied to $\operatorname{Adj}$ applied to $G$, $u_{1}$ and $v$ and walks $p$ of $v$ and $w$ to elements of $\mathrm{motive}$ applied to $u_{1}$, $w$ and $\operatorname{cons}$ applied to $h$ and $p$.
SimpleGraph.Walk.dartsdefMathlib.Combinatorics.SimpleGraph.Walk.Basic, function or constant
Wording
the dart of x (from the name)
English
Let $x$ be a walk of $u$ and $v$. Then the dart of $x$ is a list of darts of $G$ defined as $\operatorname{brecOn}$ applied to $x$ and $\mathrm{SimpleGraph\_\_Walk\_\_darts\_\_\_f}$.
SimpleGraph.Walk.edgeSetdefMathlib.Combinatorics.SimpleGraph.Walk.Basic, function or constant
Wording
the edge set of p (from the name)
English
Let $p$ be a walk of $u$ and $v$. Then the edge set of $p$ is an element of the power set of the set of symmetric squares of $V$ defined as $\operatorname{ofPred}$ applied to the function that maps $e$ to the proposition that $e$ is an element of the edge of $p$.
SimpleGraph.Walk.edgesdefMathlib.Combinatorics.SimpleGraph.Walk.Basic, function or constant
Wording
the edge of p (from the name)
English
Let $p$ be a walk of $u$ and $v$. Then the edge of $p$ is a list of symmetric squares of $V$ defined as $\operatorname{map}$ applied to $\operatorname{edge}$ and the dart of $p$.
SimpleGraph.Walk.lengthdefMathlib.Combinatorics.SimpleGraph.Walk.Basic, function or constant
Wording
the length of x (from the docstring)
English
Let $x$ be a walk of $u$ and $v$. Then the length of $x$ is a natural number defined as $\operatorname{brecOn}$ applied to $x$ and $\mathrm{SimpleGraph\_\_Walk\_\_length\_\_\_f}$.
SimpleGraph.Walk.nilconstructorMathlib.Combinatorics.SimpleGraph.Walk.Basic, function or constant
Wording
no wording
English
$\operatorname{nil}$ is a walk of $u$ and $u$.
SimpleGraph.Walk.nil'defMathlib.Combinatorics.SimpleGraph.Walk.Basic, function or constant
Wording
no wording
English
Let $u$ be an element of $V$. Then $\operatorname{nil'}$ applied to $u$ is a walk of $u$ and $u$ defined as $\operatorname{nil}$.
SimpleGraph.Walk.notNilRecdefMathlib.Combinatorics.SimpleGraph.Walk.Basic, function or constant
Wording
no wording
English
Let $\mathrm{cons}$ be a function from elements $u_{1}$ of $V$ and elements $v$ of $V$ and elements $w_{1}$ of $V$ and elements $h$ of $\mathrm{Proof}$ applied to $\operatorname{Adj}$ applied to $G$, $u_{1}$ and $v$ and walks $q$ of $v$ and $w_{1}$ to elements of $\mathrm{motive}$ applied to $u_{1}$, $w_{1}$, $\operatorname{cons}$ applied to $h$ and $q$ and $\mathrm{SimpleGraph\_\_Walk\_\_not\_nil\_cons}$. Let $p$ be a walk of $u$ and $w$ such that it is not the case that $\operatorname{Nil}$ holds for $p$. Then $\operatorname{notNilRec}$ applied to $u_{1}$, $v$, $w_{1}$, $h$, $q$, $\mathrm{cons}$, $p$ and $\mathrm{hp}$ is an element of $\mathrm{motive}$ applied to $u$, $w$, $p$ and $\mathrm{hp}$.
SimpleGraph.Walk.ofDartsdefMathlib.Combinatorics.SimpleGraph.Walk.Basic, function or constant
Wording
the walk of l (from the name)
English
Let $l$ be a list of darts of $G$ such that $l \neq \operatorname{nil}$ and $\operatorname{IsChain}$ holds for $\operatorname{DartAdj}$ applied to $G$ and $l$. Then the walk of $l$ is a walk of $\ProdfstMACRoZ {\operatorname{toProd} (\operatorname{head} (l , \mathrm{hne}))}$ and $\ProdsndMACRoAA {\operatorname{toProd} (\operatorname{getLast} (l , \mathrm{hne}))}$ defined as $\operatorname{brecOn}$ applied to $l$, $\mathrm{SimpleGraph\_\_Walk\_\_ofDarts\_\_\_f}$, $\mathrm{hne}$ and $\mathrm{hchain}$.
SimpleGraph.Walk.ofSupportdefMathlib.Combinatorics.SimpleGraph.Walk.Basic, function or constant
Wording
the walk of l (from the name)
English
Let $l$ be a list of elements of $V$ such that $l \neq \operatorname{nil}$ and $\operatorname{IsChain}$ holds for $\operatorname{Adj}$ applied to $G$ and $l$. Then the walk of $l$ is a walk of $\operatorname{head}$ applied to $l$ and $\mathrm{hne}$ and $\operatorname{getLast}$ applied to $l$ and $\mathrm{hne}$ defined as $\operatorname{brecOn}$ applied to $l$, $\mathrm{SimpleGraph\_\_Walk\_\_ofSupport\_\_\_f}$, $\mathrm{hne}$ and $\mathrm{hchain}$.
SimpleGraph.Walk.supportdefMathlib.Combinatorics.SimpleGraph.Walk.Basic, function or constant
Wording
the support of x (from the name)
English
Let $x$ be a walk of $u$ and $v$. Then the support of $x$ is a list of elements of $V$ defined as $\operatorname{brecOn}$ applied to $x$ and $\mathrm{SimpleGraph\_\_Walk\_\_support\_\_\_f}$.

Mathlib.Combinatorics.SimpleGraph.Walk.Chord

SimpleGraph.Walk.IsChorddefMathlib.Combinatorics.SimpleGraph.Walk.Chord, predicate
Wording
no wording
English
Let $p$ be a walk of $u$ and $v$. Let $e$ be a symmetric square of $V$. Then $\operatorname{IsChord}$ holds for $p$ and $e$, if $e$ is an element of the edge set for $G$, $e$ is not an element of the edge of $p$ and $\operatorname{lift}$ holds for the function that maps $v_{1}$ and $w$ to the proposition that $v_{1}$ is an element of the support of $p$ and $w$ is an element of the support of $p$ and $e$.
SimpleGraph.Walk.IsChordlessdefMathlib.Combinatorics.SimpleGraph.Walk.Chord, predicate
Wording
no wording
English
Let $p$ be a walk of $u$ and $v$. Then $\operatorname{IsChordless}$ holds for $p$, if for all symmetric squares $e$ of $V$, it is not the case that $\operatorname{IsChord}$ holds for $p$ and $e$.

Mathlib.Combinatorics.SimpleGraph.Walk.Counting

SimpleGraph.finsetWalkLengthdefMathlib.Combinatorics.SimpleGraph.Walk.Counting, function or constant
Wording
the finite set walk length of u and v (from the name)
English
Let $G$ be a simple graph of $V$. Let $n$ be a natural number. Let $u$ and $v$ be elements of $V$. Then the finite set walk length of $u$ and $v$ is a finite set of the set of walks of $u$ and $v$ defined as $\operatorname{brecOn}$ applied to $n$, $\mathrm{SimpleGraph\_\_finsetWalkLength\_\_\_f}$ applied to $G$ and $v$ and $u$.
SimpleGraph.finsetWalkLengthLTdefMathlib.Combinatorics.SimpleGraph.Walk.Counting, function or constant
Wording
no wording
English
Let $G$ be a simple graph of $V$. Let $n$ be a natural number. Let $u$ and $v$ be elements of $V$. Then $\operatorname{finsetWalkLengthLT}$ applied to $G$, $n$, $u$ and $v$ is a finite set of the set of walks of $u$ and $v$.
SimpleGraph.walkLengthTwoEquivCommonNeighborsdefMathlib.Combinatorics.SimpleGraph.Walk.Counting, function or constant
Wording
no wording
English
Let $G$ be a simple graph of $V$. Let $u$ and $v$ be elements of $V$. Then $\operatorname{walkLengthTwoEquivCommonNeighbors}$ applied to $G$, $u$ and $v$ is an element of $\EquivMACRoAE {(\SubtypeSet {p}{\mathrm{Eq} (\operatorname{length} (p), 2)})}{\operatorname{Elem} (\operatorname{commonNeighbors} (u , v))}$.

Mathlib.Combinatorics.SimpleGraph.Walk.Decomp

SimpleGraph.Walk.dropUntildefMathlib.Combinatorics.SimpleGraph.Walk.Decomp, function or constant
Wording
no wording
English
Let $p$ be a walk of $v$ and $w$. Let $u$ be an element of $V$ such that $u$ is an element of the support of $p$. Then $\operatorname{dropUntil}$ applied to $p$, $u$ and $h$ is a walk of $u$ and $w$ defined as $\operatorname{brecOn}$ applied to $p$, $\mathrm{SimpleGraph\_\_Walk\_\_dropUntil\_\_\_f}$, $u$ and $h$.
SimpleGraph.Walk.rotatedefMathlib.Combinatorics.SimpleGraph.Walk.Decomp, function or constant
Wording
no wording
English
Let $c$ be a walk of $v$ and $v$. Let $u$ be an element of $V$ such that $u$ is an element of the support of $c$. Then $\operatorname{rotate}$ applied to $c$, $u$ and $h$ is a walk of $u$ and $u$ defined as $\operatorname{append}$ applied to $\operatorname{dropUntil}$ applied to $c$, $u$ and $h$ and $\operatorname{takeUntil}$ applied to $c$, $u$ and $h$.
SimpleGraph.Walk.takeUntildefMathlib.Combinatorics.SimpleGraph.Walk.Decomp, function or constant
Wording
no wording
English
Let $p$ be a walk of $v$ and $w$. Let $u$ be an element of $V$ such that $u$ is an element of the support of $p$. Then $\operatorname{takeUntil}$ applied to $p$, $u$ and $h$ is a walk of $v$ and $u$ defined as $\operatorname{brecOn}$ applied to $p$, $\mathrm{SimpleGraph\_\_Walk\_\_takeUntil\_\_\_f}$, $u$ and $h$.

Mathlib.Combinatorics.SimpleGraph.Walk.Maps

SimpleGraph.Walk.inducedefMathlib.Combinatorics.SimpleGraph.Walk.Maps, function or constant
Wording
no wording
English
Let $s$ be an element of $\wp V$. Let $w$ be a walk of $u$ and $v$ such that for all elements $x$ of $V$, if $x$ is an element of the support of $w$, then $x$ is an element of $s$. Then $\operatorname{induce}$ applied to $s$, $w$ and $\mathrm{hw}$ is a walk of $u$ and $v$ defined as $\operatorname{brecOn}$ applied to $w$, $\mathrm{SimpleGraph\_\_Walk\_\_induce\_\_\_f}$ applied to $s$ and $\mathrm{hw}$.
SimpleGraph.Walk.mapdefMathlib.Combinatorics.SimpleGraph.Walk.Maps, function or constant
Wording
the map of f and x (from the name)
English
Let $f$ be a homomorphism of $G$ and $\mathrm{G'}$. Let $x$ be a walk of $u$ and $v$. Then the map of $f$ and $x$ is a walk of $f$ applied to $u$ and $f$ applied to $v$ defined as $\operatorname{brecOn}$ applied to $x$ and $\mathrm{SimpleGraph\_\_Walk\_\_map\_\_\_f}$ applied to $f$.
SimpleGraph.Walk.mapLedefMathlib.Combinatorics.SimpleGraph.Walk.Maps, function or constant
Wording
no wording
English
Assume that $G \leq \mathrm{G'}$. Let $p$ be a walk of $u$ and $v$. Then $\operatorname{mapLe}$ applied to $h$ and $p$ is a walk of $u$ and $v$ defined as the map of the graph homomorphism of $h$ and $p$.
SimpleGraph.Walk.toDeleteEdgedefMathlib.Combinatorics.SimpleGraph.Walk.Maps, function or constant
Wording
no wording
English
Let $e$ be a symmetric square of $V$. Let $p$ be a walk of $v$ and $w$ such that $e$ is not an element of the edge of $p$. Then $\operatorname{toDeleteEdge}$ applied to $e$, $p$ and $\mathrm{hp}$ is a walk of $v$ and $w$.
SimpleGraph.Walk.toDeleteEdgesdefMathlib.Combinatorics.SimpleGraph.Walk.Maps, function or constant
Wording
no wording
English
Let $s$ be an element of the power set of the set of symmetric squares of $V$. Let $p$ be a walk of $v$ and $w$ such that for all symmetric squares $e$ of $V$, if $e$ is an element of the edge of $p$, then $e$ is not an element of $s$. Then $\operatorname{toDeleteEdges}$ applied to $s$, $p$ and $\mathrm{hp}$ is a walk of $v$ and $w$.
SimpleGraph.Walk.transferdefMathlib.Combinatorics.SimpleGraph.Walk.Maps, function or constant
Wording
the transfer of p and H (from the name)
English
Let $p$ be a walk of $u$ and $v$. Let $H$ be a simple graph of $V$ such that for all symmetric squares $e$ of $V$, if $e$ is an element of the edge of $p$, then $e$ is an element of the edge set for $H$. Then the transfer of $p$ and $H$ is a walk of $u$ and $v$ defined as $\operatorname{brecOn}$ applied to $p$, $\mathrm{SimpleGraph\_\_Walk\_\_transfer\_\_\_f}$ applied to $H$ and $h$.

Mathlib.Combinatorics.SimpleGraph.Walk.Operations

SimpleGraph.Walk.appenddefMathlib.Combinatorics.SimpleGraph.Walk.Operations, function or constant
Wording
no wording
English
Let $x$ be a walk of $u$ and $v$. Let $x_{1}$ be a walk of $v$ and $w$. Then $\operatorname{append}$ applied to $x$ and $x_{1}$ is a walk of $u$ and $w$ defined as $\operatorname{brecOn}$ applied to $x$, $\mathrm{SimpleGraph\_\_Walk\_\_append\_\_\_f}$ and $x_{1}$.
SimpleGraph.Walk.concatdefMathlib.Combinatorics.SimpleGraph.Walk.Operations, function or constant
Wording
no wording
English
Let $p$ be a walk of $u$ and $v$. Assume that $\operatorname{Adj}$ holds for $G$, $v$ and $w$. Then $\operatorname{concat}$ applied to $p$ and $h$ is a walk of $u$ and $w$ defined as $\operatorname{append}$ applied to $p$ and $\operatorname{cons}$ applied to $h$ and $\operatorname{nil}$.
SimpleGraph.Walk.concatRecdefMathlib.Combinatorics.SimpleGraph.Walk.Operations, function or constant
Wording
no wording
English
Let $\mathrm{Hnil}$ be a function from elements $u_{2}$ of $V$ to elements of $\mathrm{motive}$ applied to $u_{2}$, $u_{2}$ and $\operatorname{nil}$. Let $\mathrm{Hconcat}$ be a function from elements $u_{1}$ of $V$ and elements $v_{1}$ of $V$ and elements $w$ of $V$ and walks $p_{1}$ of $u_{1}$ and $v_{1}$ and elements $h$ of $\mathrm{Proof}$ applied to $\operatorname{Adj}$ applied to $G$, $v_{1}$ and $w$ and elements of $\mathrm{motive}$ applied to $u_{1}$, $v_{1}$ and $p_{1}$ to elements of $\mathrm{motive}$ applied to $u_{1}$, $w$ and $\operatorname{concat}$ applied to $p_{1}$ and $h$. Let $p$ be a walk of $u$ and $v$. Then $\operatorname{concatRec}$ applied to $u_{2}$, $\mathrm{Hnil}$, $u_{1}$, $v_{1}$, $w$, $p_{1}$, $h$, $\mathrm{Hconcat}$ and $p$ is an element of $\mathrm{motive}$ applied to $u$, $v$ and $p$.
SimpleGraph.Walk.copydefMathlib.Combinatorics.SimpleGraph.Walk.Operations, function or constant
Wording
the copy of p (from the name)
English
Let $p$ be a walk of $u$ and $v$. Assume that $\EqtMACRoH {u}{\mathrm{u'}}$. Assume that $\EqtMACRoH {v}{\mathrm{v'}}$. Then the copy of $p$ is a walk of $\mathrm{u'}$ and $\mathrm{v'}$.
SimpleGraph.Walk.dropdefMathlib.Combinatorics.SimpleGraph.Walk.Operations, function or constant
Wording
no wording
English
Let $p$ be a walk of $u$ and $v$. Let $n$ be a natural number. Then $\operatorname{drop}$ applied to $p$ and $n$ is a walk of $\operatorname{getVert}$ applied to $p$ and $n$ and $v$ defined as $\operatorname{brecOn}$ applied to $p$, $\mathrm{SimpleGraph\_\_Walk\_\_drop\_\_\_f}$ and $n$.
SimpleGraph.Walk.dropLastdefMathlib.Combinatorics.SimpleGraph.Walk.Operations, function or constant
Wording
no wording
English
Let $p$ be a walk of $u$ and $v$. Then $\operatorname{dropLast}$ applied to $p$ is a walk of $u$ and the penultimate vertex of $p$ defined as $\operatorname{take}$ applied to $p$ and the difference between the length of $p$ and $1$.
SimpleGraph.Walk.reversedefMathlib.Combinatorics.SimpleGraph.Walk.Operations, function or constant
Wording
the walk in reverse of w (from the docstring)
English
Let $w$ be a walk of $u$ and $v$. Then the walk in reverse of $w$ is a walk of $v$ and $u$ defined as $\operatorname{reverseAux}$ applied to $w$ and $\operatorname{nil}$.
SimpleGraph.Walk.taildefMathlib.Combinatorics.SimpleGraph.Walk.Operations, function or constant
Wording
the tail of p (from the name)
English
Let $p$ be a walk of $u$ and $v$. Then the tail of $p$ is a walk of the second vertex of $p$ and $v$ defined as $\operatorname{drop}$ applied to $p$ and $1$.
SimpleGraph.Walk.takedefMathlib.Combinatorics.SimpleGraph.Walk.Operations, function or constant
Wording
no wording
English
Let $p$ be a walk of $u$ and $v$. Let $n$ be a natural number. Then $\operatorname{take}$ applied to $p$ and $n$ is a walk of $u$ and $\operatorname{getVert}$ applied to $p$ and $n$ defined as $\operatorname{brecOn}$ applied to $p$, $\mathrm{SimpleGraph\_\_Walk\_\_take\_\_\_f}$ and $n$.

Mathlib.Combinatorics.SimpleGraph.Walk.Subwalks

SimpleGraph.Walk.IsSubwalkdefMathlib.Combinatorics.SimpleGraph.Walk.Subwalks, predicate
Wording
no wording
English
Let $p$ be a walk of $x$ and $x_{1}$. Let $q$ be a walk of $x_{2}$ and $x_{3}$. Then $\operatorname{IsSubwalk}$ holds for $p$ and $q$, if there exists a walk $\mathrm{ru}$ of $x_{2}$ and $x$, such that there exists a walk $\mathrm{rv}$ of $x_{1}$ and $x_{3}$, such that $\EqtMACRoH {q}{\operatorname{append} (\operatorname{append} (\mathrm{ru} , p), \mathrm{rv})}$.

Mathlib.Combinatorics.SimpleGraph.Walk.Traversal

SimpleGraph.Walk.firstDartdefMathlib.Combinatorics.SimpleGraph.Walk.Traversal, function or constant
Wording
the first dart of p and hp (from the docstring)
English
Let $p$ be a walk of $v$ and $w$ such that it is not the case that $\operatorname{Nil}$ holds for $p$. Then the first dart of $p$ and $\mathrm{hp}$ is a dart of $G$ defined as $\operatorname{mk}$ applied to $\ProdmkMACRoU {v}{\operatorname{snd} (p)}$ and $\mathrm{SimpleGraph\_\_Walk\_\_adj\_snd}$ applied to $\mathrm{hp}$.
SimpleGraph.Walk.getVertdefMathlib.Combinatorics.SimpleGraph.Walk.Traversal, function or constant
Wording
no wording
English
Let $x$ be a walk of $u$ and $v$. Let $x_{1}$ be a natural number. Then $\operatorname{getVert}$ applied to $x$ and $x_{1}$ is an element of $V$ defined as $\operatorname{brecOn}$ applied to $x$, $\mathrm{SimpleGraph\_\_Walk\_\_getVert\_\_\_f}$ and $x_{1}$.
SimpleGraph.Walk.lastDartdefMathlib.Combinatorics.SimpleGraph.Walk.Traversal, function or constant
Wording
the last dart of p and hp (from the docstring)
English
Let $p$ be a walk of $v$ and $w$ such that it is not the case that $\operatorname{Nil}$ holds for $p$. Then the last dart of $p$ and $\mathrm{hp}$ is a dart of $G$ defined as $\operatorname{mk}$ applied to $\ProdmkMACRoU {\operatorname{penultimate} (p)}{w}$ and $\mathrm{SimpleGraph\_\_Walk\_\_adj\_penultimate}$ applied to $\mathrm{hp}$.
SimpleGraph.Walk.penultimatedefMathlib.Combinatorics.SimpleGraph.Walk.Traversal, function or constant
Wording
the penultimate vertex of p (from the docstring)
English
Let $p$ be a walk of $u$ and $v$. Then the penultimate vertex of $p$ is an element of $V$ defined as $\operatorname{getVert}$ applied to $p$ and the difference between the length of $p$ and $1$.
SimpleGraph.Walk.snddefMathlib.Combinatorics.SimpleGraph.Walk.Traversal, function or constant
Wording
the second vertex of p (from the docstring)
English
Let $p$ be a walk of $u$ and $v$. Then the second vertex of $p$ is an element of $V$ defined as $\operatorname{getVert}$ applied to $p$ and $1$.

Mathlib.Combinatorics.Tiling.Tile

DiscreteTiling.PlacedTilestructureMathlib.Combinatorics.Tiling.Tile, type
Wording
no wording
English
Let $\mathrm{ps}$ be a protoset of $X$ and $x$. Then the elements of $\operatorname{PlacedTile}$ applied to $\mathrm{ps}$ are a basic type.
DiscreteTiling.PlacedTile.coeSetdefMathlib.Combinatorics.Tiling.Tile, function or constant
Wording
the coercion set of pt (from the name)
English
Let $\mathrm{pt}$ be an element of $\operatorname{PlacedTile}$ applied to $\mathrm{ps}$. Then the coercion set of $\mathrm{pt}$ is an element of $\wp X$.
DiscreteTiling.PlacedTile.groupEltsdefMathlib.Combinatorics.Tiling.Tile, function or constant
Wording
no wording
English
Let $\mathrm{self}$ be an element of $\operatorname{PlacedTile}$ applied to $\mathrm{ps}$. Then $\operatorname{groupElts}$ applied to $\mathrm{self}$ is a quotient of $G$ and the map of the subtype of the stabilizer of $G$ and the carrier of the tile of $\mathrm{ps}$ and the index of the tile in the protoset of $\mathrm{self}$ and the symmetry of the tile of $\mathrm{ps}$ and the index of the tile in the protoset of $\mathrm{self}$ defined as $\operatorname{proj1}$ applied to $\mathrm{self}$.
DiscreteTiling.PlacedTile.indexdefMathlib.Combinatorics.Tiling.Tile, function or constant
Wording
the index of the tile in the protoset of self (from the docstring)
English
Let $\mathrm{self}$ be an element of $\operatorname{PlacedTile}$ applied to $\mathrm{ps}$. Then the index of the tile in the protoset of $\mathrm{self}$ is an element of $x$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.
DiscreteTiling.ProtosetstructureMathlib.Combinatorics.Tiling.Tile, type
Wording
protoset of X and x (from the name)
English
Let $G$, $X$ and $x$ be sets. Then the protosets of $X$ and $x$ are a basic type.
DiscreteTiling.Protoset.tilesdefMathlib.Combinatorics.Tiling.Tile, function or constant
Wording
the tile of self and x3 (from the name)
English
Let $\mathrm{self}$ be a protoset of $X$ and $x$. Let $x_{3}$ be an element of $x$. Then the tile of $\mathrm{self}$ and $x_{3}$ is an element of $\operatorname{Prototile}$ applied to $G$ and $X$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$ and $x_{3}$.
DiscreteTiling.PrototilestructureMathlib.Combinatorics.Tiling.Tile, type
Wording
no wording
English
Let $G$ and $X$ be sets. Then the elements of $\operatorname{Prototile}$ applied to $G$ and $X$ are a basic type.
DiscreteTiling.Prototile.carrierdefMathlib.Combinatorics.Tiling.Tile, function or constant
Wording
the carrier of self (from the name)
English
Let $\mathrm{self}$ be an element of $\operatorname{Prototile}$ applied to $G$ and $X$. Then the carrier of $\mathrm{self}$ is an element of $\wp X$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.
DiscreteTiling.Prototile.symmetriesdefMathlib.Combinatorics.Tiling.Tile, function or constant
Wording
the symmetry of self (from the name)
English
Let $\mathrm{self}$ be an element of $\operatorname{Prototile}$ applied to $G$ and $X$. Then the symmetry of $\mathrm{self}$ is a subgroup of $\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {\operatorname{stabilizer} (G , \operatorname{carrier} (\mathrm{self}))}{x_{2}})}$ defined as $\operatorname{proj1}$ applied to $\mathrm{self}$.

Mathlib.Combinatorics.Young.SemistandardTableau

SemistandardYoungTableaustructureMathlib.Combinatorics.Young.SemistandardTableau, type
Wording
no wording
English
Let $x$ be an element of $\mathrm{YoungDiagram}$. Then the elements of $\mathrm{SemistandardYoungTableau}$ applied to $x$ are a basic type.
SemistandardYoungTableau.copydefMathlib.Combinatorics.Young.SemistandardTableau, function or constant
Wording
the copy of T and h (from the name)
English
Let $T$ be an element of $\mathrm{SemistandardYoungTableau}$ applied to $x$. Let $\mathrm{entry'}$ be a function from natural numbers and natural numbers to natural numbers such that $\mathrm{entry'}$ is equal to $\operatorname{coe}$ applied to $T$. Then the copy of $T$ and $\mathrm{entry'}$ is an element of $\mathrm{SemistandardYoungTableau}$ applied to $x$.
SemistandardYoungTableau.entrydefMathlib.Combinatorics.Young.SemistandardTableau, function or constant
Wording
the entry of x1 and x2 (from the name)
English
Let $\mathrm{self}$ be an element of $\mathrm{SemistandardYoungTableau}$ applied to $x$. Let $x_{1}$ and $x_{2}$ be natural numbers. Then the entry of $x_{1}$ and $x_{2}$ is a natural number defined as $\operatorname{proj0}$ applied to $\mathrm{self}$, $x_{1}$ and $x_{2}$.
SemistandardYoungTableau.highestWeightdefMathlib.Combinatorics.Young.SemistandardTableau, function or constant
Wording
no wording
English
Let $x$ be an element of $\mathrm{YoungDiagram}$. Then $\operatorname{highestWeight}$ applied to $x$ is an element of $\mathrm{SemistandardYoungTableau}$ applied to $x$.

Mathlib.Combinatorics.Young.YoungDiagram

YoungDiagramstructureMathlib.Combinatorics.Young.YoungDiagram, type
Wording
no wording
English
The elements of $\mathrm{YoungDiagram}$ are a basic type.
YoungDiagram.carddefMathlib.Combinatorics.Young.YoungDiagram, function or constant
Wording
the cardinality of x (from the name)
English
Let $x$ be an element of $\mathrm{YoungDiagram}$. Then the cardinality of $x$ is a natural number defined as the cardinality of the cell of $x$.
YoungDiagram.cellsdefMathlib.Combinatorics.Young.YoungDiagram, function or constant
Wording
the cell of self (from the name)
English
Let $\mathrm{self}$ be an element of $\mathrm{YoungDiagram}$. Then the cell of $\mathrm{self}$ is a finite set of $\mathrm{Prod}$ applied to $\Natural$ and $\Natural$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.
YoungDiagram.cellsOfRowLensdefMathlib.Combinatorics.Young.YoungDiagram, function or constant
Wording
the cell of x (from the name)
English
Let $x$ be a list of natural numbers. Then the cell of $x$ is a finite set of $\mathrm{Prod}$ applied to $\Natural$ and $\Natural$ defined as $\operatorname{brecOn}$ applied to $x$ and $\mathrm{YoungDiagram\_\_cellsOfRowLens\_\_\_f}$.
YoungDiagram.coldefMathlib.Combinatorics.Young.YoungDiagram, function or constant
Wording
no wording
English
Let $x$ be an element of $\mathrm{YoungDiagram}$. Let $j$ be an element of $\Natural$. Then $\operatorname{col}$ applied to $x$ and $j$ is a finite set of $\mathrm{Prod}$ applied to $\Natural$ and $\Natural$ defined as $\FinsetFilter {c}{\mathrm{Eq} (\ProdsndMACRoAA {c}, j)}{\operatorname{cells} (x)}$.
YoungDiagram.colLendefMathlib.Combinatorics.Young.YoungDiagram, function or constant
Wording
no wording
English
Let $x$ be an element of $\mathrm{YoungDiagram}$. Let $j$ be a natural number. Then $\operatorname{colLen}$ applied to $x$ and $j$ is a natural number defined as $\operatorname{find}$ applied to $\mathrm{YoungDiagram\_\_exists\_notMem\_col}$ applied to $x$ and $j$.
YoungDiagram.equivListRowLensdefMathlib.Combinatorics.Young.YoungDiagram, function or constant
Wording
no wording
English
$\operatorname{equivListRowLens}$ is an equivalence from $\mathrm{YoungDiagram}$ to $\SubtypeSet {w}{\mathrm{and} (\operatorname{SortedGE} (w), \mathrm{forall} (\Natural , \lambda x . \mathrm{if} (\MembershipmemMACRoT {w}{x}, \mathrm{Lt} (0 , x))))}$.
YoungDiagram.ofRowLensdefMathlib.Combinatorics.Young.YoungDiagram, function or constant
Wording
no wording
English
Let $w$ be a list of natural numbers such that $\operatorname{SortedGE}$ holds for $w$. Then $\operatorname{ofRowLens}$ applied to $w$ and $\mathrm{hw}$ is an element of $\mathrm{YoungDiagram}$.
YoungDiagram.rowdefMathlib.Combinatorics.Young.YoungDiagram, function or constant
Wording
the row of x and i (from the name)
English
Let $x$ be an element of $\mathrm{YoungDiagram}$. Let $i$ be an element of $\Natural$. Then the row of $x$ and $i$ is a finite set of $\mathrm{Prod}$ applied to $\Natural$ and $\Natural$ defined as $\FinsetFilter {c}{\mathrm{Eq} (\ProdfstMACRoZ {c}, i)}{\operatorname{cells} (x)}$.
YoungDiagram.rowLendefMathlib.Combinatorics.Young.YoungDiagram, function or constant
Wording
no wording
English
Let $x$ be an element of $\mathrm{YoungDiagram}$. Let $i$ be a natural number. Then $\operatorname{rowLen}$ applied to $x$ and $i$ is a natural number defined as $\operatorname{find}$ applied to $\mathrm{YoungDiagram\_\_exists\_notMem\_row}$ applied to $x$ and $i$.
YoungDiagram.rowLensdefMathlib.Combinatorics.Young.YoungDiagram, function or constant
Wording
no wording
English
Let $x$ be an element of $\mathrm{YoungDiagram}$. Then $\operatorname{rowLens}$ applied to $x$ is a list of natural numbers defined as $\operatorname{map}$ applied to $\operatorname{rowLen}$ applied to $x$ and $\operatorname{range}$ applied to $\operatorname{colLen}$ applied to $x$ and $0$.
YoungDiagram.transposedefMathlib.Combinatorics.Young.YoungDiagram, function or constant
Wording
the transpose of x (from the name)
English
Let $x$ be an element of $\mathrm{YoungDiagram}$. Then the transpose of $x$ is an element of $\mathrm{YoungDiagram}$.
YoungDiagram.transposeOrderIsodefMathlib.Combinatorics.Young.YoungDiagram, function or constant
Wording
the transpose order isomorphism (from the name)
English
The transpose order isomorphism is an order isomorphism of $\mathrm{YoungDiagram}$ and $\mathrm{YoungDiagram}$.

‹ previous next ›