Definitions: Mathlib.Combinatorics, part 2 of 3

Quiver.Path.addWeightdefMathlib.Combinatorics.Quiver.Path.Weight, function or constant

Wording

no wording

English

Let $w$ be a function from elements $i_{1}$ of $V$ and elements $j_{1}$ of $V$ and homomorphisms of $i_{1}$ and $j_{1}$ to elements of $R$. Let $x_{2}$ be a path of $i$ and $j$. Then $\operatorname{addWeight}$ applied to $i_{1}$, $j_{1}$, $w$ and $x_{2}$ is an element of $R$ defined as the function that maps $w$ and $x_{2}$ to $\mathrm{Quiver\_\_Path\_\_addWeight\_\_\_unary}$ applied to $i_{1}$, $\operatorname{mk}$ applied to $i$ and $\operatorname{mk}$ applied to $j$ and $j_{1}$, $w$ and $x_{2}$.

Quiver.Path.addWeightOfEPsdefMathlib.Combinatorics.Quiver.Path.Weight, function or constant

Wording

no wording

English

Let $w$ be a function from elements of $V$ and elements of $V$ to elements of $R$. Let $x_{2}$ be a path of $i$ and $j$. Then $\operatorname{addWeightOfEPs}$ applied to $w$ and $x_{2}$ is an element of $R$ defined as $\operatorname{addWeight}$ applied to the function that maps $i_{1}$, $j_{1}$ and $x_{2}$ to $w$ applied to $i_{1}$ and $j_{1}$ and $x_{2}$.

Quiver.Path.weightdefMathlib.Combinatorics.Quiver.Path.Weight, function or constant

Wording

no wording

English

Let $w$ be a function from elements $i_{1}$ of $V$ and elements $j_{1}$ of $V$ and homomorphisms of $i_{1}$ and $j_{1}$ to elements of $R$. Let $x_{2}$ be a path of $i$ and $j$. Then $\operatorname{weight}$ applied to $i_{1}$, $j_{1}$, $w$ and $x_{2}$ is an element of $R$ defined as the function that maps $w$ and $x_{2}$ to $\mathrm{Quiver\_\_Path\_\_weight\_\_\_unary}$ applied to $i_{1}$, $\operatorname{mk}$ applied to $i$ and $\operatorname{mk}$ applied to $j$ and $j_{1}$, $w$ and $x_{2}$.

Quiver.Path.weightOfEPsdefMathlib.Combinatorics.Quiver.Path.Weight, function or constant

Wording

no wording

English

Let $w$ be a function from elements of $V$ and elements of $V$ to elements of $R$. Let $x_{2}$ be a path of $i$ and $j$. Then $\operatorname{weightOfEPs}$ applied to $w$ and $x_{2}$ is an element of $R$ defined as $\operatorname{weight}$ applied to the function that maps $i_{1}$, $j_{1}$ and $x_{2}$ to $w$ applied to $i_{1}$ and $j_{1}$ and $x_{2}$.

Mathlib.Combinatorics.Quiver.Prefunctor

PrefunctorstructureMathlib.Combinatorics.Quiver.Prefunctor, type

Wording

prefunctor of V and W (from the name)

English

Let $V$ and $W$ be sets. Then the prefunctors of $V$ and $W$ are a basic type.

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

Wording

the composition of F and G (from the name)

English

Let $F$ be a prefunctor of $U$ and $V$. Let $G$ be a prefunctor of $V$ and $W$. Then the composition of $F$ and $G$ is a prefunctor of $U$ and $W$ defined as $\operatorname{mk}$ applied to the function that maps $X$ to the object of $G$ and the object of $F$ and $X$ and the function that maps $x_{3}$, $x_{4}$ and $f$ to the map of $G$ and the map of $F$ and $f$.

Prefunctor.iddefMathlib.Combinatorics.Quiver.Prefunctor, function or constant

Wording

the identity of V (from the name)

English

Let $V$ be a set. Then the identity of $V$ is a prefunctor of $V$ and $V$ defined as $\operatorname{mk}$ applied to the function that maps $X$ to $X$ and the function that maps $x_{1}$, $x_{2}$ and $f$ to $f$.

Prefunctor.mapdefMathlib.Combinatorics.Quiver.Prefunctor, function or constant

Wording

the map of self and x2 (from the name)

English

Let $\mathrm{self}$ be a prefunctor of $V$ and $W$. Let $x_{2}$ be a homomorphism of $X$ and $Y$. Then the map of $\mathrm{self}$ and $x_{2}$ is a homomorphism of the object of $\mathrm{self}$ and $X$ and the object of $\mathrm{self}$ and $Y$ defined as $\operatorname{proj1}$ applied to $\mathrm{self}$ and $x_{2}$.

Prefunctor.objdefMathlib.Combinatorics.Quiver.Prefunctor, function or constant

Wording

the object of self and x2 (from the name)

English

Let $\mathrm{self}$ be a prefunctor of $V$ and $W$. Let $x_{2}$ be an element of $V$. Then the object of $\mathrm{self}$ and $x_{2}$ is an element of $W$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$ and $x_{2}$.

Mathlib.Combinatorics.Quiver.Push

Quiver.PushdefMathlib.Combinatorics.Quiver.Push, type

Wording

no wording

English

Let $x$ be a function from elements of $V$ to elements of $W$. Then an element of $\operatorname{Push}$ applied to $x$ is an element of the function that maps $x$ to $W$.

Quiver.Push.liftdefMathlib.Combinatorics.Quiver.Push, function or constant

Wording

the lift of x3 and x4 (from the name)

English

Let $x_{1}$ be a function from elements of $V$ to elements of $W$. Let $x_{3}$ be a prefunctor of $V$ and $\mathrm{W'}$. Let $x_{4}$ be a function from elements of $W$ to elements of $\mathrm{W'}$ such that for all elements $x_{5}$ of $V$, the object of $x_{3}$ and $x_{5}$ is equal to $x_{4}$ applied to $x_{1}$ applied to $x_{5}$. Then the lift of $x_{3}$ and $x_{4}$ is a prefunctor of $\operatorname{Push}$ applied to $x_{1}$ and $\mathrm{W'}$.

Quiver.Push.ofdefMathlib.Combinatorics.Quiver.Push, function or constant

Wording

no wording

English

Let $x_{1}$ be a function from elements of $V$ to elements of $W$. Then $\operatorname{of}$ applied to $x_{1}$ is a prefunctor of $V$ and $\operatorname{Push}$ applied to $x_{1}$ defined as $\operatorname{mk}$ applied to $x_{1}$ and the function that maps $x_{2}$, $x_{3}$ and $f$ to the arrow of $f$.

Quiver.PushQuiverinductiveMathlib.Combinatorics.Quiver.Push, type

Wording

no wording

English

Let $x_{1}$ be a function from elements of $V$ to elements of $W$. Let $x_{2}$ and $x_{3}$ be elements of $W$. Then the elements of $\operatorname{PushQuiver}$ applied to $x_{1}$, $x_{2}$ and $x_{3}$ are a basic type.

Quiver.PushQuiver.arrowconstructorMathlib.Combinatorics.Quiver.Push, function or constant

Wording

the arrow of f (from the name)

English

Let $f$ be a homomorphism of $X$ and $Y$. Then the arrow of $f$ is an element of $\operatorname{PushQuiver}$ applied to $x_{1}$, $x_{1}$ applied to $X$ and $x_{1}$ applied to $Y$.

Mathlib.Combinatorics.Quiver.ReflQuiver

CategoryTheory.Functor.toReflPrefunctordefMathlib.Combinatorics.Quiver.ReflQuiver, function or constant

Wording

the identity prefunctor of F (from the name)

English

Let $F$ be a functor of $C$ and $D$. Then the identity prefunctor of $F$ is an identity prefunctor of $C$ and $D$ defined as $\operatorname{mk}$ applied to $\operatorname{mk}$ applied to $\operatorname{obj}$ applied to $F$ and $\operatorname{map}$ applied to $F$ and $\mathrm{CategoryTheory\_\_Functor\_\_map\_id}$ applied to $F$.

CategoryTheory.ReflPrefunctorstructureMathlib.Combinatorics.Quiver.ReflQuiver, type

Wording

identity prefunctor of V and W (from the name)

English

Let $V$ and $W$ be sets. Then the identity prefunctors of $V$ and $W$ are a basic type.

CategoryTheory.ReflPrefunctor.compdefMathlib.Combinatorics.Quiver.ReflQuiver, function or constant

Wording

the composition of F and G (from the name)

English

Let $F$ be an identity prefunctor of $U$ and $V$. Let $G$ be an identity prefunctor of $V$ and $W$. Then the composition of $F$ and $G$ is an identity prefunctor of $U$ and $W$.

CategoryTheory.ReflPrefunctor.iddefMathlib.Combinatorics.Quiver.ReflQuiver, function or constant

Wording

the identity of V (from the name)

English

Let $V$ be a set. Then the identity of $V$ is an identity prefunctor of $V$ and $V$.

CategoryTheory.ReflQuiverclassMathlib.Combinatorics.Quiver.ReflQuiver, predicate

Wording

obj is a identity quiver (from the name)

English

Let $\mathrm{obj}$ be a set. Then we can say that $\mathrm{obj}$ is an identity quiver.

CategoryTheory.ReflQuiver.iddefMathlib.Combinatorics.Quiver.ReflQuiver, function or constant

Wording

the identity morphism of X (from the docstring)

English

Let $X$ be an element of $\mathrm{obj}$. Then the identity morphism of $X$ is a homomorphism of $X$ and $X$ defined as $\operatorname{proj1}$ applied to $\mathrm{self}$ and $X$.

Mathlib.Combinatorics.Quiver.Schreier

Quiver.SchreierGraphstructureMathlib.Combinatorics.Quiver.Schreier, type

Wording

no wording

English

Let $V$ be a set. Let $x_{1}$ be a function from elements of $S$ to elements of $M$. Then the elements of $\operatorname{SchreierGraph}$ applied to $V$ and $x_{1}$ are a basic type.

Quiver.SchreierGraph.equivdefMathlib.Combinatorics.Quiver.Schreier, function or constant

Wording

the equivalence of V and x1 (from the name)

English

Let $V$ be a set. Let $x_{1}$ be a function from elements of $S$ to elements of $M$. Then the equivalence of $V$ and $x_{1}$ is an element of $\EquivMACRoAE {V}{\operatorname{SchreierGraph} (V , x_{1})}$.

Quiver.SchreierGraph.evalWorddefMathlib.Combinatorics.Quiver.Schreier, function or constant

Wording

the evaluation word of x1 and w (from the name)

English

Let $x_{1}$ be a function from elements of $S$ to elements of $M$. Let $w$ be a list of elements of $\mathrm{Prod}$ applied to $S$ and $\mathrm{Bool}$. Then the evaluation word of $x_{1}$ and $w$ is an element of $M$ defined as $\operatorname{coe}$ applied to the lift, $x_{1}$ and $\operatorname{mk}$ applied to $w$.

Quiver.SchreierGraph.labellingdefMathlib.Combinatorics.Quiver.Schreier, function or constant

Wording

the labelling of V and x1 (from the name)

English

Let $V$ be a set. Let $x_{1}$ be a function from elements of $S$ to elements of $M$. Then the labelling of $V$ and $x_{1}$ is a prefunctor of $\operatorname{SchreierGraph}$ applied to $V$ and $x_{1}$ and the set of single objects of $S$ defined as $\operatorname{mk}$ applied to the function that maps $x_{2}$ to the star of $S$ and the function that maps $x_{3}$, $x_{4}$ and $e$ to $e$.

Quiver.SchreierGraph.labellingCostarEquivdefMathlib.Combinatorics.Quiver.Schreier, function or constant

Wording

the costar map of the labelling prefunctor of x2 and x3 (from the docstring)

English

Let $x_{2}$ be a function from elements of $S$ to elements of $M$. Let $x_{3}$ be an element of $\operatorname{SchreierGraph}$ applied to $V$ and $x_{2}$. Then the costar map of the labelling prefunctor of $x_{2}$ and $x_{3}$ is an equivalence from $\operatorname{Costar}$ applied to $x_{3}$ to $\operatorname{Costar}$ applied to the star of $S$.

Quiver.SchreierGraph.labellingStarEquivdefMathlib.Combinatorics.Quiver.Schreier, function or constant

Wording

the star map of the labelling prefunctor of x2 and x3 (from the docstring)

English

Let $x_{2}$ be a function from elements of $S$ to elements of $M$. Let $x_{3}$ be an element of $\operatorname{SchreierGraph}$ applied to $V$ and $x_{2}$. Then the star map of the labelling prefunctor of $x_{2}$ and $x_{3}$ is an equivalence from the set of stars of $x_{3}$ to the set of stars of the star of $S$.

Quiver.SchreierGraph.pathFromWorddefMathlib.Combinatorics.Quiver.Schreier, function or constant

Wording

the path from word of x3 and w (from the name)

English

Let $x_{2}$ be a function from elements of $S$ to elements of $M$. Let $x_{3}$ be an element of $\operatorname{SchreierGraph}$ applied to $V$ and $x_{2}$. Let $w$ be a list of elements of $\mathrm{Prod}$ applied to $S$ and $\mathrm{Bool}$. Then the path from word of $x_{3}$ and $w$ is a path of the object of $\operatorname{of}$ and $x_{3}$ and the object of $\operatorname{of}$ and $\HSMulhSMulMACRoAL {\operatorname{evalWord} (x_{2} , w)}{x_{3}}$ defined as $\operatorname{brecOn}$ applied to $w$ and $\mathrm{Quiver\_\_SchreierGraph\_\_pathFromWord\_\_\_f}$ applied to $x_{2}$ and $x_{3}$.

Quiver.SchreierGraph.toVertexdefMathlib.Combinatorics.Quiver.Schreier, function or constant

Wording

the underlying vertex of self (from the docstring)

English

Let $\mathrm{self}$ be an element of $\operatorname{SchreierGraph}$ applied to $V$ and $x_{1}$. Then the underlying vertex of $\mathrm{self}$ is an element of $V$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.

Mathlib.Combinatorics.Quiver.SingleObj

Quiver.SingleObjdefMathlib.Combinatorics.Quiver.SingleObj, type

Wording

single object of x (from the name)

English

Let $x$ be a set. Then a single object of $x$ is an element of the function that maps $x$ to $\mathrm{Unit}$.

Quiver.SingleObj.pathEquivListdefMathlib.Combinatorics.Quiver.SingleObj, function or constant

Wording

the path equivalence list (from the name)

English

The path equivalence list is an equivalence from the set of paths of the star of $x$ and the star of $x$ to the set of lists of elements of $x$.

Quiver.SingleObj.stardefMathlib.Combinatorics.Quiver.SingleObj, function or constant

Wording

the star of x (from the name)

English

Let $x$ be a set. Then the star of $x$ is a single object of $x$ defined as $\operatorname{default}$.

Quiver.SingleObj.toHomdefMathlib.Combinatorics.Quiver.SingleObj, function or constant

Wording

the homomorphism (from the name)

English

The homomorphism is an equivalence from $x$ to the set of homomorphisms of the star of $x$ and the star of $x$ defined as the identity of $x$.

Quiver.SingleObj.toPrefunctordefMathlib.Combinatorics.Quiver.SingleObj, function or constant

Wording

the prefunctor (from the name)

English

The prefunctor is an equivalence from the set of functions from elements of $x$ to elements of $x_{1}$ to the set of prefunctors of the set of single objects of $x$ and the set of single objects of $x_{1}$.

Mathlib.Combinatorics.Quiver.Subquiver

Quiver.LabellingdefMathlib.Combinatorics.Quiver.Subquiver, type

Wording

labelling of V and L (from the name)

English

Let $V$ and $L$ be sets. Then a labelling of $V$ and $L$ is an element of the function that maps $V$ and $L$ to the set of functions from elements $a$ of $V$ and elements $b$ of $V$ and homomorphisms of $a$ and $b$ to elements of $L$.

Quiver.TotalstructureMathlib.Combinatorics.Quiver.Subquiver, type

Wording

no wording

English

Let $V$ be a set. Then the elements of $\operatorname{Total}$ applied to $V$ are a basic type.

Quiver.Total.homdefMathlib.Combinatorics.Quiver.Subquiver, function or constant

Wording

the homomorphism of self (from the name)

English

Let $\mathrm{self}$ be an element of $\operatorname{Total}$ applied to $V$. Then the homomorphism of $\mathrm{self}$ is a homomorphism of the left of $\mathrm{self}$ and the right of $\mathrm{self}$ defined as $\operatorname{proj2}$ applied to $\mathrm{self}$.

Quiver.Total.leftdefMathlib.Combinatorics.Quiver.Subquiver, function or constant

Wording

the left of self (from the name)

English

Let $\mathrm{self}$ be an element of $\operatorname{Total}$ applied to $V$. Then the left of $\mathrm{self}$ is an element of $V$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.

Quiver.Total.rightdefMathlib.Combinatorics.Quiver.Subquiver, function or constant

Wording

the right of self (from the name)

English

Let $\mathrm{self}$ be an element of $\operatorname{Total}$ applied to $V$. Then the right of $\mathrm{self}$ is an element of $V$ defined as $\operatorname{proj1}$ applied to $\mathrm{self}$.

Quiver.wideSubquiverEquivSetTotaldefMathlib.Combinatorics.Quiver.Subquiver, function or constant

Wording

no wording

English

$\operatorname{wideSubquiverEquivSetTotal}$ is an equivalence from the set of wide subquivers of $V$ to $\wp \operatorname{Total} (V)$.

WideSubquiverdefMathlib.Combinatorics.Quiver.Subquiver, type

Wording

wide subquiver of V (from the name)

English

Let $V$ be a set. Then a wide subquiver of $V$ is an element of the function that maps $V$ to the set of functions from elements $a$ of $V$ and elements $b$ of $V$ to elements of the power set of the set of homomorphisms of $a$ and $b$.

WideSubquiver.toTypedefMathlib.Combinatorics.Quiver.Subquiver, type

Wording

type of V and x1 (from the name)

English

Let $V$ be a set. Let $x_{1}$ be a wide subquiver of $V$. Then a type of $V$ and $x_{1}$ is an element of the function that maps $V$ and $x_{1}$ to $V$.

Mathlib.Combinatorics.Quiver.Symmetric

Prefunctor.MapReverseclassMathlib.Combinatorics.Quiver.Symmetric, predicate

Wording

x4 is a map reverse (from the name)

English

Let $x_{4}$ be a prefunctor of $U$ and $V$. Then we can say that $x_{4}$ is a map reverse.

Prefunctor.symmetrifydefMathlib.Combinatorics.Quiver.Symmetric, function or constant

Wording

no wording

English

Let $x_{2}$ be a prefunctor of $U$ and $V$. Then $\operatorname{symmetrify}$ applied to $x_{2}$ is a prefunctor of $\operatorname{Symmetrify}$ applied to $U$ and $\operatorname{Symmetrify}$ applied to $V$ defined as $\operatorname{mk}$ applied to $\operatorname{obj}$ applied to $x_{2}$ and the function that maps $x_{3}$ and $x_{4}$ to $\operatorname{map}$ applied to $\operatorname{map}$ applied to $x_{2}$ and $\operatorname{map}$ applied to $x_{2}$.

Quiver.HasInvolutiveReverseclassMathlib.Combinatorics.Quiver.Symmetric, predicate

Wording

V has involutive reverses (from the name)

English

Let $V$ be a set. Then we can say that $V$ has involutive reverses.

Quiver.HasReverseclassMathlib.Combinatorics.Quiver.Symmetric, predicate

Wording

V has reverses (from the name)

English

Let $V$ be a set. Then we can say that $V$ has reverses.

Quiver.HasReverse.reverse'defMathlib.Combinatorics.Quiver.Symmetric, function or constant

Wording

the reverse of x1 (from the name)

English

Let $x_{1}$ be a homomorphism of $a$ and $b$. Then the reverse of $x_{1}$ is a homomorphism of $b$ and $a$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$ and $x_{1}$.

Quiver.Hom.toNegdefMathlib.Combinatorics.Quiver.Symmetric, function or constant

Wording

the negation of f (from the name)

English

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

Quiver.Hom.toPosdefMathlib.Combinatorics.Quiver.Symmetric, function or constant

Wording

the positive part of f (from the name)

English

Let $f$ be a homomorphism of $X$ and $Y$. Then the positive part of $f$ is a homomorphism of $X$ and $Y$ defined as $\operatorname{inl}$ applied to $f$.

Quiver.Path.reversedefMathlib.Combinatorics.Quiver.Symmetric, function or constant

Wording

the reverse of x2 (from the name)

English

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

Quiver.SymmetrifydefMathlib.Combinatorics.Quiver.Symmetric, type

Wording

no wording

English

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

Quiver.Symmetrify.liftdefMathlib.Combinatorics.Quiver.Symmetric, function or constant

Wording

the lift of x3 (from the name)

English

Let $x_{3}$ be a prefunctor of $V$ and $\mathrm{V'}$. Then the lift of $x_{3}$ is a prefunctor of $\operatorname{Symmetrify}$ applied to $V$ and $\mathrm{V'}$.

Quiver.Symmetrify.ofdefMathlib.Combinatorics.Quiver.Symmetric, function or constant

Wording

no wording

English

$\operatorname{of}$ is a prefunctor of $V$ and $\operatorname{Symmetrify}$ applied to $V$ defined as $\operatorname{mk}$ applied to $\mathrm{id}$ and the function that maps $x_{1}$ and $x_{2}$ to $\operatorname{inl}$.

Quiver.reversedefMathlib.Combinatorics.Quiver.Symmetric, function or constant

Wording

the reverse of x2 (from the name)

English

Let $x_{2}$ be a homomorphism of $a$ and $b$. Then the reverse of $x_{2}$ is a homomorphism of $b$ and $a$ defined as the reverse of $x_{2}$.

Mathlib.Combinatorics.Schnirelmann

schnirelmannDensitydefMathlib.Combinatorics.Schnirelmann, function or constant

Wording

no wording

English

Let $A$ be an element of $\wp \Natural$. Then $\mathrm{schnirelmannDensity}$ applied to $A$ is a real number defined as the infimum of the function that maps $n$ to $\frac{ \FinsetcardMACRoM {(\FinsetFilter {a}{(\MembershipmemMACRoT {A}{a})}{(\FinsetIocMACRoAI {0}{n})})}}{n}$.

Mathlib.Combinatorics.SetFamily.AhlswedeZhang

AhlswedeZhang.infSumdefMathlib.Combinatorics.SetFamily.AhlswedeZhang, function or constant

Wording

the infimum sum of x3 (from the name)

English

Let $x_{3}$ be a finite set of the set of finite sets of $x$. Then the infimum sum of $x_{3}$ is an element of $\Rational$ defined as $\FinsetSum {\FinsetunivMACRoAC}{s}{(\frac{ \FinsetcardMACRoM {\operatorname{truncatedInf} (x_{3} , s)}}{\FinsetcardMACRoM {s}\times \operatorname{choose} (\operatorname{card} (x), \FinsetcardMACRoM {s})})}$.

AhlswedeZhang.supSumdefMathlib.Combinatorics.SetFamily.AhlswedeZhang, function or constant

Wording

the supremum sum of x3 (from the name)

English

Let $x_{3}$ be a finite set of the set of finite sets of $x$. Then the supremum sum of $x_{3}$ is an element of $\Rational$ defined as $\FinsetSum {\FinsetunivMACRoAC}{s}{(\frac{ \FinsetcardMACRoM {\operatorname{truncatedSup} (x_{3} , s)}}{(\operatorname{card} (x)- \FinsetcardMACRoM {s})\times \operatorname{choose} (\operatorname{card} (x), \FinsetcardMACRoM {s})})}$.

Finset.truncatedInfdefMathlib.Combinatorics.SetFamily.AhlswedeZhang, function or constant

Wording

the truncated infimum of s and a (from the name)

English

Let $s$ be a finite set of $x$. Let $a$ be an element of $x$. Then the truncated infimum of $s$ and $a$ is an element of $x$.

Finset.truncatedSupdefMathlib.Combinatorics.SetFamily.AhlswedeZhang, function or constant

Wording

the truncated supremum of s and a (from the name)

English

Let $s$ be a finite set of $x$. Let $a$ be an element of $x$. Then the truncated supremum of $s$ and $a$ is an element of $x$.

Mathlib.Combinatorics.SetFamily.Compression.Down

Down.compressiondefMathlib.Combinatorics.SetFamily.Compression.Down, function or constant

Wording

no wording

English

Let $a$ be an element of $x$. Let $x_{2}$ be a finite set of the set of finite sets of $x$. Then $\operatorname{compression}$ applied to $a$ and $x_{2}$ is a finite set of the set of finite sets of $x$.

Finset.memberSubfamilydefMathlib.Combinatorics.SetFamily.Compression.Down, function or constant

Wording

no wording

English

Let $a$ be an element of $x$. Let $x_{2}$ be a finite set of the set of finite sets of $x$. Then $\operatorname{memberSubfamily}$ applied to $a$ and $x_{2}$ is a finite set of the set of finite sets of $x$ defined as the forward image of $\FinsetFilter {s_{1}}{(\MembershipmemMACRoT {s_{1}}{a})}{x_{2}}$ under the function that maps $s$ to $\operatorname{erase}$ applied to $s$ and $a$.

Finset.nonMemberSubfamilydefMathlib.Combinatorics.SetFamily.Compression.Down, function or constant

Wording

no wording

English

Let $a$ be an element of $x$. Let $x_{2}$ be a finite set of the set of finite sets of $x$. Then $\operatorname{nonMemberSubfamily}$ applied to $a$ and $x_{2}$ is a finite set of the set of finite sets of $x$ defined as $\FinsetFilter {s}{\mathrm{not} (\MembershipmemMACRoT {s}{a})}{x_{2}}$.

Mathlib.Combinatorics.SetFamily.Compression.UV

UV.IsCompresseddefMathlib.Combinatorics.SetFamily.Compression.UV, predicate

Wording

no wording

English

Let $u$ and $v$ be elements of $x$. Let $s$ be a finite set of $x$. Then $\operatorname{IsCompressed}$ holds for $u$, $v$ and $s$, if $\EqtMACRoH {\operatorname{compression} (u , v , s)}{s}$.

UV.compressdefMathlib.Combinatorics.SetFamily.Compression.UV, function or constant

Wording

no wording

English

Let $u$, $v$ and $a$ be elements of $x$. Then $\operatorname{compress}$ applied to $u$, $v$ and $a$ is an element of $x$ defined as $\iteMACRoG {\mathrm{and} (\mathrm{Disjoint} (u , a), \mathrm{Leq} (v , a))}{\operatorname{sdiff} (\MaxmaxMACRoAF {a}{u}, v)}{a}$.

UV.compressiondefMathlib.Combinatorics.SetFamily.Compression.UV, function or constant

Wording

no wording

English

Let $u$ and $v$ be elements of $x$. Let $s$ be a finite set of $x$. Then $\operatorname{compression}$ applied to $u$, $v$ and $s$ is a finite set of $x$ defined as $\UnionunionMACRoAB {(\FinsetFilter {a}{(\MembershipmemMACRoT {s}{\operatorname{compress} (u , v , a)})}{s})}{(\FinsetFilter {a_{1}}{\mathrm{not} (\MembershipmemMACRoT {s}{a_{1}})}{\operatorname{image} (s , \operatorname{compress} (u , v))})}$.

Mathlib.Combinatorics.SetFamily.DualVC

Finset.dualFamilydefMathlib.Combinatorics.SetFamily.DualVC, function or constant

Wording

the dual family of x2 and X (from the name)

English

Let $x_{2}$ be a finite set of the set of finite sets of $x$. Let $X$ be a finite set of $x$. Then the dual family of $x_{2}$ and $X$ is a finite set of the set of finite sets of the set of finite sets of $x$ defined as the forward image of $X$ under the function that maps $x_{3}$ to $\FinsetFilter {A}{(\MembershipmemMACRoT {A}{x_{3}})}{x_{2}}$.

Mathlib.Combinatorics.SetFamily.Intersecting

Set.IntersectingdefMathlib.Combinatorics.SetFamily.Intersecting, predicate

Wording

no wording

English

Let $s$ be an element of $\wp x$. Then $\operatorname{Intersecting}$ 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 $a$ is not disjoint to $b$.

Set.IsIntersectingOfdefMathlib.Combinatorics.SetFamily.Intersecting, predicate

Wording

no wording

English

Let $L$ be an element of $\wp \Natural$. Let $x_{2}$ be an element of the power set of the set of finite sets of $x$. Then $\operatorname{IsIntersectingOf}$ holds for $L$ and $x_{2}$, if $\operatorname{Pairwise}$ holds for $x_{2}$ and the function that maps $s$ and $t$ to $\MembershipmemMACRoT {L}{\FinsetcardMACRoM {\operatorname{inter} (s , t)}}$.

Mathlib.Combinatorics.SetFamily.LYM

Finset.fallingdefMathlib.Combinatorics.SetFamily.LYM, function or constant

Wording

no wording

English

Let $k$ be a natural number. Let $x_{2}$ be a finite set of the set of finite sets of $x$. Then $\operatorname{falling}$ applied to $k$ and $x_{2}$ is a finite set of the set of finite sets of $x$ defined as the supremum of $x_{2}$ and $\operatorname{powersetCard}$ applied to $k$.

Mathlib.Combinatorics.SetFamily.Shadow

Finset.shadowdefMathlib.Combinatorics.SetFamily.Shadow, function or constant

Wording

no wording

English

Let $x_{2}$ be a finite set of the set of finite sets of $x$. Then $\operatorname{shadow}$ applied to $x_{2}$ is a finite set of the set of finite sets of $x$ defined as the supremum of $x_{2}$ and the function that maps $s$ to the forward image of $s$ under $\operatorname{erase}$ applied to $s$.

Finset.upShadowdefMathlib.Combinatorics.SetFamily.Shadow, function or constant

Wording

no wording

English

Let $x_{3}$ be a finite set of the set of finite sets of $x$. Then $\operatorname{upShadow}$ applied to $x_{3}$ is a finite set of the set of finite sets of $x$ defined as the supremum of $x_{3}$ and the function that maps $s$ to the forward image of the complement of $s$ under the function that maps $a$ to $\operatorname{insert}$ applied to $a$ and $s$.

Mathlib.Combinatorics.SetFamily.Shatter

Finset.ShattersdefMathlib.Combinatorics.SetFamily.Shatter, predicate

Wording

no wording

English

Let $x_{2}$ be a finite set of the set of finite sets of $x$. Let $s$ be a finite set of $x$. Then $\operatorname{Shatters}$ holds for $x_{2}$ and $s$, if for all finite sets $t$ of $x$, if $t \leq s$, then there exists a finite set $u$ of $x$, such that $u$ is an element of $x_{2}$ and $\EqtMACRoH {\operatorname{inter} (s , u)}{t}$.

Finset.shattererdefMathlib.Combinatorics.SetFamily.Shatter, function or constant

Wording

no wording

English

Let $x_{2}$ be a finite set of the set of finite sets of $x$. Then $\operatorname{shatterer}$ applied to $x_{2}$ is a finite set of the set of finite sets of $x$ defined as $\FinsetFilter {s}{\operatorname{Shatters} (x_{2} , s)}{\operatorname{biUnion} (x_{2} , \operatorname{powerset})}$.

Finset.vcDimdefMathlib.Combinatorics.SetFamily.Shatter, function or constant

Wording

no wording

English

Let $x_{2}$ be a finite set of the set of finite sets of $x$. Then $\operatorname{vcDim}$ applied to $x_{2}$ is a natural number defined as the supremum of $\operatorname{shatterer}$ applied to $x_{2}$ and $\FinsetcardMACRoM$.

Mathlib.Combinatorics.SimpleGraph.Acyclic

SimpleGraph.IsAcyclicdefMathlib.Combinatorics.SimpleGraph.Acyclic, predicate

Wording

G is acyclic (from the name)

English

Let $G$ be a simple graph of $V$. Then $G$ is acyclic, if for all elements $v$ of $V$, for all walks $c$ of $v$ and $v$, $c$ is not a cycle.

SimpleGraph.IsAcyclic.coloringTwodefMathlib.Combinatorics.SimpleGraph.Acyclic, function or constant

Wording

no wording

English

Assume that $G$ is acyclic. Then $\operatorname{coloringTwo}$ applied to $\mathrm{hG}$ is a coloring of $G$ and $\mathrm{Fin}$ applied to $2$.

SimpleGraph.IsAcyclic.coloringTwoOfVertsdefMathlib.Combinatorics.SimpleGraph.Acyclic, function or constant

Wording

no wording

English

Assume that $G$ is acyclic. Let $\mathrm{verts}$ be a function from connected components of $G$ to elements of $V$ such that for all connected components $C$ of $G$, $\MembershipmemMACRoT {C}{\mathrm{verts} (C)}$. Then $\operatorname{coloringTwoOfVerts}$ applied to $\mathrm{hG}$, $\mathrm{verts}$ and $h$ is a coloring of $G$ and $\mathrm{Fin}$ applied to $2$.

SimpleGraph.IsTreestructureMathlib.Combinatorics.SimpleGraph.Acyclic, predicate

Wording

G is a tree (from the name)

English

Let $G$ be a simple graph of $V$. Then we can say that $G$ is a tree.

SimpleGraph.IsTree.coloringTwodefMathlib.Combinatorics.SimpleGraph.Acyclic, function or constant

Wording

no wording

English

Assume that $G$ is a tree. Then $\operatorname{coloringTwo}$ applied to $\mathrm{hG}$ is a coloring of $G$ and $\mathrm{Fin}$ applied to $2$.

SimpleGraph.IsTree.coloringTwoOfVertdefMathlib.Combinatorics.SimpleGraph.Acyclic, function or constant

Wording

no wording

English

Assume that $G$ is a tree. Let $u$ be an element of $V$. Then $\operatorname{coloringTwoOfVert}$ applied to $\mathrm{hG}$ and $u$ is a coloring of $G$ and $\mathrm{Fin}$ applied to $2$.

Mathlib.Combinatorics.SimpleGraph.AdjMatrix

Matrix.IsAdjMatrixstructureMathlib.Combinatorics.SimpleGraph.AdjMatrix, predicate

Wording

A is a adjoint matrix (from the name)

English

Let $A$ be a matrix of $V$ and $x$. Then we can say that $A$ is an adjoint matrix.

Matrix.IsAdjMatrix.toGraphdefMathlib.Combinatorics.SimpleGraph.AdjMatrix, function or constant

Wording

the graph of h1 (from the name)

English

Assume that $A$ is an adjoint matrix. Then the graph of $h_{1}$ is a simple graph of $V$.

Matrix.IsAdjMatrix.toGraphReindexIsodefMathlib.Combinatorics.SimpleGraph.AdjMatrix, function or constant

Wording

the graph reindexing isomorphism of A and f (from the name)

English

Let $A$ be a matrix of $V$ and $x$ such that $A$ is an adjoint matrix. Let $f$ be an equivalence from $V$ to $W$. Then the graph reindexing isomorphism of $A$ and $f$ is an isomorphism of the graph of $\operatorname{reindex}$ applied to $h_{1}$ and $f$ and the graph of $h_{1}$.

Matrix.IsAdjMatrix.toGraphSubmatrixEmbeddingdefMathlib.Combinatorics.SimpleGraph.AdjMatrix, function or constant

Wording

the graph submatrix embedding of A and f (from the name)

English

Let $A$ be a matrix of $V$ and $x$ such that $A$ is an adjoint matrix. Let $f$ be an embedding of $W$ and $V$. Then the graph submatrix embedding of $A$ and $f$ is an embedding of the graph of $\operatorname{submatrix}$ applied to $h_{1}$ and $\operatorname{coe}$ applied to $f$ and the graph of $h_{1}$.

Matrix.IsAdjMatrix.toGraphSubmatrixHomdefMathlib.Combinatorics.SimpleGraph.AdjMatrix, function or constant

Wording

the graph submatrix homomorphism of A and f (from the name)

English

Let $A$ be a matrix of $V$ and $x$ such that $A$ is an adjoint matrix. Let $f$ be a function from elements of $W$ to elements of $V$. Then the graph submatrix homomorphism of $A$ and $f$ is a homomorphism of the graph of $\operatorname{submatrix}$ applied to $h_{1}$ and $f$ and the graph of $h_{1}$.

Matrix.compldefMathlib.Combinatorics.SimpleGraph.AdjMatrix, function or constant

Wording

the complement of A (from the name)

English

Let $A$ be a matrix of $V$ and $x$. Then the complement of $A$ is a matrix of $V$ and $x$ defined as $\operatorname{of}$ applied to the function that maps $i_{1}$ and $j_{1}$ to $\iteMACRoG {(\EqtMACRoH {i_{1}}{j_{1}})}{0}{(\iteMACRoG {(\EqtMACRoH {A (i_{1} , j_{1})}{0})}{1}{0})}$.

SimpleGraph.adjMatrixdefMathlib.Combinatorics.SimpleGraph.AdjMatrix, function or constant

Wording

the matrix of x and G (from the docstring)

English

Let $x$ be a set. Let $G$ be a simple graph of $V$. Then the matrix of $x$ and $G$ is a matrix of $V$ and $x$ defined as $\operatorname{of}$ applied to the function that maps $i_{1}$ and $j_{1}$ to $\iteMACRoG {\operatorname{Adj} (G , i_{1} , j_{1})}{1}{0}$.

Mathlib.Combinatorics.SimpleGraph.Basic

SimpleGraphstructureMathlib.Combinatorics.SimpleGraph.Basic, type

Wording

simple graph of V (from the name)

English

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

SimpleGraph.AdjdefMathlib.Combinatorics.SimpleGraph.Basic, predicate

Wording

no wording

English

Let $\mathrm{self}$ be a simple graph 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}$.

SimpleGraph.IsCompleteBetweendefMathlib.Combinatorics.SimpleGraph.Basic, predicate

Wording

no wording

English

Let $G$ be a simple graph of $V$. Let $s$ and $t$ be elements of $\wp V$. Then $\operatorname{IsCompleteBetween}$ holds for $G$, $s$ and $t$, if for all elements $x$ of $V$, if $x$ is an element of $s$, then for all elements $x_{1}$ of $V$, if $x_{1}$ is an element of $t$, then $\operatorname{Adj}$ holds for $G$, $x$ and $x_{1}$.

SimpleGraph.IsIsolateddefMathlib.Combinatorics.SimpleGraph.Basic, predicate

Wording

G is isolated (from the docstring)

English

Let $G$ be a simple graph of $V$. Let $v$ be an element of $V$. Then $G$ is isolated, if for all elements $w$ of $V$, it is not the case that $\operatorname{Adj}$ holds for $G$, $v$ and $w$.

SimpleGraph.IsUniversaldefMathlib.Combinatorics.SimpleGraph.Basic, predicate

Wording

G is universal (from the docstring)

English

Let $G$ be a simple graph of $V$. Let $v$ be an element of $V$. Then $G$ is universal, if for all elements $w$ of $V$, if $v \neq w$, then $\operatorname{Adj}$ holds for $G$, $v$ and $w$.

SimpleGraph.commonNeighborsdefMathlib.Combinatorics.SimpleGraph.Basic, function or constant

Wording

the common neighbor of v and w (from the name)

English

Let $G$ be a simple graph of $V$. Let $v$ and $w$ be elements of $V$. Then the common neighbor of $v$ and $w$ is an element of $\wp V$ defined as $\operatorname{inter}$ applied to the neighbor set of $G$ and $v$ and the neighbor set of $G$ and $w$.

SimpleGraph.completeGraphdefMathlib.Combinatorics.SimpleGraph.Basic, function or constant

Wording

the complete graph of V (from the name)

English

Let $V$ be a set. Then the complete graph of $V$ is a simple graph of $V$ defined as the top.

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

Wording

the edge set for G (from the docstring)

English

Let $G$ be a simple graph of $V$. Then the edge set for $G$ is an element of the power set of the set of symmetric squares of $V$ defined as $\operatorname{edgeSetEmbedding}$ applied to $V$ and $G$.

SimpleGraph.edgeSetEmbeddingdefMathlib.Combinatorics.SimpleGraph.Basic, function or constant

Wording

the edge set embedding of V (from the name)

English

Let $V$ be a set. Then the edge set embedding of $V$ is an order embedding of the set of simple graphs of $V$ and the power set of the set of symmetric squares of $V$.

SimpleGraph.emptyGraphdefMathlib.Combinatorics.SimpleGraph.Basic, function or constant

Wording

the empty graph of V (from the name)

English

Let $V$ be a set. Then the empty graph of $V$ is a simple graph of $V$ defined as the bottom.

SimpleGraph.fromEdgeSetdefMathlib.Combinatorics.SimpleGraph.Basic, function or constant

Wording

no wording

English

Let $s$ be an element of the power set of the set of symmetric squares of $V$. Then $\operatorname{fromEdgeSet}$ applied to $s$ is a simple graph of $V$.

SimpleGraph.fromReldefMathlib.Combinatorics.SimpleGraph.Basic, function or constant

Wording

no wording

English

Let $r$ be a function from elements of $V$ and elements of $V$ to propositions. Then $\operatorname{fromRel}$ applied to $r$ is a simple graph of $V$.

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

Wording

the incidence set 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 incidence set of $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 for $G$ and $v$ is an element of $e$.

SimpleGraph.incidenceSetEquivNeighborSetdefMathlib.Combinatorics.SimpleGraph.Basic, function or constant

Wording

the incidence set equivalence neighbor set 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 incidence set equivalence neighbor set of $G$ and $v$ is an equivalence from the set of elements of the incidence set of $G$ and $v$ to the set of elements of the neighbor set of $G$ and $v$.

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

Wording

no wording

English

$\operatorname{mk'}$ is an embedding of $\SubtypeSet {\mathrm{adj}}{\mathrm{and} (\mathrm{forall} (V , \lambda x . \mathrm{forall} (V , \lambda y . \EqtMACRoH {\mathrm{adj} (x , y)}{\mathrm{adj} (y , x)})), \mathrm{forall} (V , \lambda x_{1} . \mathrm{not} (\EqtMACRoH {\mathrm{adj} (x_{1} , x_{1})}{\operatorname{true}})))}$ and the set of simple graphs of $V$.

SimpleGraph.neighborSetdefMathlib.Combinatorics.SimpleGraph.Basic, function or constant

Wording

the neighbor set 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 neighbor set of $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 $G$, $v$ and $w$.

SimpleGraph.otherVertexOfIncidentdefMathlib.Combinatorics.SimpleGraph.Basic, function or constant

Wording

the other vertex of G and h (from the name)

English

Let $G$ be a simple graph of $V$ such that $e$ is an element of the incidence set of $G$ and $v$. Then the other vertex of $G$ and $h$ is an element of $V$.

SimpleGraph.supportdefMathlib.Combinatorics.SimpleGraph.Basic, function or constant

Wording

the support of G (from the name)

English

Let $G$ be a simple graph of $V$. Then the support of $G$ is an element of $\wp V$.

aesop_graphdefMathlib.Combinatorics.SimpleGraph.Basic, function or constant

Wording

no wording

English

generation took over the time limit

aesop_graph?defMathlib.Combinatorics.SimpleGraph.Basic, function or constant

Wording

no wording

English

generation took over the time limit

aesop_graph_nonterminaldefMathlib.Combinatorics.SimpleGraph.Basic, function or constant

Wording

no wording

English

generation took over the time limit

completeBipartiteGraphdefMathlib.Combinatorics.SimpleGraph.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 simple graph of $\mathrm{Sum}$ applied to $V$ and $W$.

Mathlib.Combinatorics.SimpleGraph.Bipartite

SimpleGraph.Copy.completeBipartiteGraphdefMathlib.Combinatorics.SimpleGraph.Bipartite, function or constant

Wording

the complete bipartite graph of left and right (from the name)

English

Let $\mathrm{left}$ and $\mathrm{right}$ be finite sets of $V$ such that the cardinality of $\mathrm{left}$ is equal to the cardinality of $x$, the cardinality of $\mathrm{right}$ is equal to the cardinality of $x_{1}$ and $\operatorname{IsCompleteBetween}$ holds for $G$, $\mathrm{left}$ and $\mathrm{right}$. Then the complete bipartite graph of $\mathrm{left}$ and $\mathrm{right}$ is a copy of the complete bipartite graph of $x$ and $x_{1}$ and $G$.

SimpleGraph.IsBipartitedefMathlib.Combinatorics.SimpleGraph.Bipartite, predicate

Wording

G is bipartite (from the name)

English

Let $G$ be a simple graph of $V$. Then $G$ is bipartite, if $\operatorname{Colorable}$ holds for $G$ and $2$.

SimpleGraph.IsBipartiteWithstructureMathlib.Combinatorics.SimpleGraph.Bipartite, predicate

Wording

no wording

English

Let $G$ be a simple graph of $V$. Let $s$ and $t$ be elements of $\wp V$. Then we can say that $\operatorname{IsBipartiteWith}$ holds for $G$, $s$ and $t$.

SimpleGraph.IsBipartiteWith.edgeSetEmbeddingCompleteBipartiteGraphdefMathlib.Combinatorics.SimpleGraph.Bipartite, function or constant

Wording

the edge set embedding complete bipartite graph of hG (from the name)

English

Assume that $\operatorname{IsBipartiteWith}$ holds for $G$, $s$ and $t$. Then the edge set embedding complete bipartite graph of $\mathrm{hG}$ is an embedding of the set of elements of the edge set for $G$ and the set of elements of the edge set for the complete bipartite graph of the set of elements of $s$ and the set of elements of $t$.

SimpleGraph.betweendefMathlib.Combinatorics.SimpleGraph.Bipartite, function or constant

Wording

no wording

English

Let $s$ and $t$ be elements of $\wp V$. Let $G$ be a simple graph of $V$. Then $\operatorname{between}$ applied to $s$, $t$ and $G$ is a simple graph of $V$.

SimpleGraph.bipartiteDoubleCoverdefMathlib.Combinatorics.SimpleGraph.Bipartite, function or constant

Wording

the bipartite double cover of G (from the name)

English

Let $G$ be a simple graph of $V$. Then the bipartite double cover of $G$ is a simple graph of $\mathrm{Sum}$ applied to $V$ and $V$.

Mathlib.Combinatorics.SimpleGraph.Cayley

SimpleGraph.addCayleydefMathlib.Combinatorics.SimpleGraph.Cayley, function or constant

Wording

the Cayley graph induced by an operation of s (from the docstring)

English

Let $s$ be an element of $\wp M$. Then the Cayley graph induced by an operation of $s$ is a simple graph of $M$ defined as $\operatorname{fromRel}$ applied to the function that maps $x_{1}$ and $x_{2}$ to the proposition that there exists an element $g$ of $M$, such that $g$ is an element of $s$ and $\EqtMACRoH {x_{1} + g}{x_{2}}$.

SimpleGraph.mulCayleydefMathlib.Combinatorics.SimpleGraph.Cayley, function or constant

Wording

the Cayley graph induced by an operation of s (from the docstring)

English

Mathlib.Combinatorics.SimpleGraph.Circulant

SimpleGraph.circulantGraphdefMathlib.Combinatorics.SimpleGraph.Circulant, function or constant

Wording

the circulant graph of s (from the name)

English

Let $s$ be an element of $\wp G$. Then the circulant graph of $s$ is a simple graph of $G$ defined as $\operatorname{fromRel}$ applied to the function that maps $x_{1}$ and $x_{2}$ to $\MembershipmemMACRoT {s}{(x_{1} - x_{2})}$.

Mathlib.Combinatorics.SimpleGraph.Clique

SimpleGraph.CliqueFreedefMathlib.Combinatorics.SimpleGraph.Clique, predicate

Wording

no wording

English

Let $G$ be a simple graph of $x$. Let $n$ be a natural number. Then $\operatorname{CliqueFree}$ holds for $G$ and $n$, if for all finite sets $t$ of $x$, it is not the case that $\operatorname{IsNClique}$ holds for $G$, $n$ and $t$.

SimpleGraph.CliqueFreeOndefMathlib.Combinatorics.SimpleGraph.Clique, predicate

Wording

no wording

English

Let $G$ be a simple graph of $x$. Let $s$ be an element of $\wp x$. Let $n$ be a natural number. Then $\operatorname{CliqueFreeOn}$ holds for $G$, $s$ and $n$, if for all finite sets $t$ of $x$, if $t \leq s$, then it is not the case that $\operatorname{IsNClique}$ holds for $G$, $n$ and $t$.

SimpleGraph.IndepSetFreedefMathlib.Combinatorics.SimpleGraph.Clique, predicate

Wording

no wording

English

Let $G$ be a simple graph of $x$. Let $n$ be a natural number. Then $\operatorname{IndepSetFree}$ holds for $G$ and $n$, if for all finite sets $t$ of $x$, it is not the case that $\operatorname{IsNIndepSet}$ holds for $G$, $n$ and $t$.

SimpleGraph.IndepSetFreeOndefMathlib.Combinatorics.SimpleGraph.Clique, predicate

Wording

no wording

English

Let $G$ be a simple graph of $x$. Let $s$ be an element of $\wp x$. Let $n$ be a natural number. Then $\operatorname{IndepSetFreeOn}$ holds for $G$, $s$ and $n$, if for all finite sets $t$ of $x$, if $t \leq s$, then it is not the case that $\operatorname{IsNIndepSet}$ holds for $G$, $n$ and $t$.

SimpleGraph.IsCliquedefMathlib.Combinatorics.SimpleGraph.Clique, predicate

Wording

no wording

English

Let $G$ be a simple graph of $x$. Let $s$ be an element of $\wp x$. Then $\operatorname{IsClique}$ holds for $G$ and $s$, if $\operatorname{Pairwise}$ holds for $s$ and $\operatorname{Adj}$ applied to $G$.

SimpleGraph.IsIndepSetdefMathlib.Combinatorics.SimpleGraph.Clique, predicate

Wording

no wording

English

Let $G$ be a simple graph of $x$. Let $s$ be an element of $\wp x$. Then $\operatorname{IsIndepSet}$ holds for $G$ and $s$, if $\operatorname{Pairwise}$ holds for $s$ and the function that maps $v$ and $w$ to the proposition that it is not the case that $\operatorname{Adj}$ holds for $G$, $v$ and $w$.

SimpleGraph.IsMaximumCliquestructureMathlib.Combinatorics.SimpleGraph.Clique, predicate

Wording

no wording

English

Let $G$ be a simple graph of $x$. Let $s$ be a finite set of $x$. Then we can say that $\operatorname{IsMaximumClique}$ holds for $G$ and $s$.

SimpleGraph.IsMaximumIndepSetstructureMathlib.Combinatorics.SimpleGraph.Clique, predicate

Wording

no wording

English

Let $G$ be a simple graph of $x$. Let $s$ be a finite set of $x$. Then we can say that $\operatorname{IsMaximumIndepSet}$ holds for $G$ and $s$.

SimpleGraph.IsNCliquestructureMathlib.Combinatorics.SimpleGraph.Clique, predicate

Wording

no wording

English

Let $G$ be a simple graph of $x$. Let $n$ be a natural number. Let $s$ be a finite set of $x$. Then we can say that $\operatorname{IsNClique}$ holds for $G$, $n$ and $s$.

SimpleGraph.IsNIndepSetstructureMathlib.Combinatorics.SimpleGraph.Clique, predicate

Wording

no wording

English

Let $G$ be a simple graph of $x$. Let $n$ be a natural number. Let $s$ be a finite set of $x$. Then we can say that $\operatorname{IsNIndepSet}$ holds for $G$, $n$ and $s$.

SimpleGraph.cliqueFinsetdefMathlib.Combinatorics.SimpleGraph.Clique, function or constant

Wording

the clique finite set of G and n (from the name)

English

Let $G$ be a simple graph of $x$. Let $n$ be a natural number. Then the clique finite set of $G$ and $n$ is a finite set of the set of finite sets of $x$ defined as $\FinsetFilter {s}{\operatorname{IsNClique} (G , n , s)}{\FinsetunivMACRoAC}$.

SimpleGraph.cliqueNumdefMathlib.Combinatorics.SimpleGraph.Clique, function or constant

Wording

the clique numerator of G (from the name)

English

Let $G$ be a simple graph of $x$. Then the clique numerator of $G$ is a natural number defined as the supremum of $\operatorname{ofPred}$ applied to the function that maps $n$ to the proposition that there exists a finite set $s$ of $x$, such that $\operatorname{IsNClique}$ holds for $G$, $n$ and $s$.

SimpleGraph.cliqueSetdefMathlib.Combinatorics.SimpleGraph.Clique, function or constant

Wording

the clique set of G and n (from the name)

English

Let $G$ be a simple graph of $x$. Let $n$ be a natural number. Then the clique set of $G$ and $n$ is an element of the power set of the set of finite sets of $x$ defined as $\operatorname{ofPred}$ applied to the function that maps $s$ to $\operatorname{IsNClique}$ applied to $G$, $n$ and $s$.

SimpleGraph.completeMultipartiteGraph.topEmbeddingdefMathlib.Combinatorics.SimpleGraph.Clique, function or constant

Wording

the top embedding of V and f (from the name)

English

Let $V$ be a function from elements of $x$ to sets. Let $f$ be a function from elements $i$ of $x$ to elements of $V$ applied to $i$. Then the top embedding of $V$ and $i$ is an embedding of the top and the complete multipartite graph of $V$.

SimpleGraph.indepNumdefMathlib.Combinatorics.SimpleGraph.Clique, function or constant

Wording

the independent numerator of G (from the name)

English

Let $G$ be a simple graph of $x$. Then the independent numerator of $G$ is a natural number defined as the supremum of $\operatorname{ofPred}$ applied to the function that maps $n$ to the proposition that there exists a finite set $s$ of $x$, such that $\operatorname{IsNIndepSet}$ holds for $G$, $n$ and $s$.

SimpleGraph.indepSetFinsetdefMathlib.Combinatorics.SimpleGraph.Clique, function or constant

Wording

the independent set finite set of G and n (from the name)

English

Let $G$ be a simple graph of $x$. Let $n$ be a natural number. Then the independent set finite set of $G$ and $n$ is a finite set of the set of finite sets of $x$ defined as $\FinsetFilter {s}{\operatorname{IsNIndepSet} (G , n , s)}{\FinsetunivMACRoAC}$.

SimpleGraph.indepSetSetdefMathlib.Combinatorics.SimpleGraph.Clique, function or constant

Wording

the independent set set of G and n (from the name)

English

Let $G$ be a simple graph of $x$. Let $n$ be a natural number. Then the independent set set of $G$ and $n$ is an element of the power set of the set of finite sets of $x$ defined as $\operatorname{ofPred}$ applied to the function that maps $s$ to $\operatorname{IsNIndepSet}$ applied to $G$, $n$ and $s$.

SimpleGraph.topEmbeddingOfNotCliqueFreedefMathlib.Combinatorics.SimpleGraph.Clique, function or constant

Wording

the top embedding of h (from the name)

English

Assume that it is not the case that $\operatorname{CliqueFree}$ holds for $G$ and $n$. Then the top embedding of $h$ is an embedding of the complete graph of $\mathrm{Fin}$ applied to $n$ and $G$.

Mathlib.Combinatorics.SimpleGraph.Coloring.Constructions

SimpleGraph.Coloring.completeEquipartiteGraphdefMathlib.Combinatorics.SimpleGraph.Coloring.Constructions, function or constant

Wording

the complete equipartite graph (from the name)

English

The complete equipartite graph is a coloring of the complete equipartite graph of $r$ and $t$ and $\mathrm{Fin}$ applied to $r$.

SimpleGraph.Coloring.turanGraphdefMathlib.Combinatorics.SimpleGraph.Coloring.Constructions, function or constant

Wording

the Turan graph of n and r (from the name)

English

Let $n$ and $r$ be natural numbers. Then the Turan graph of $n$ and $r$ is a coloring of the Turan graph of $n$ and $r$ and $\mathrm{Fin}$ applied to $r$.

SimpleGraph.cycleGraph.bicoloring_of_evendefMathlib.Combinatorics.SimpleGraph.Coloring.Constructions, function or constant

Wording

no wording

English

Let $n$ be an even natural number. Then $\mathrm{SimpleGraph\_\_cycleGraph\_\_bicoloring\_of\_even}$ applied to $n$ and $h$ is a coloring of the cycle graph of $n$ and $\mathrm{Bool}$.

SimpleGraph.cycleGraph.tricoloringdefMathlib.Combinatorics.SimpleGraph.Coloring.Constructions, function or constant

Wording

no wording

English

Let $n$ be a natural number such that $2 \leq n$. Then $\operatorname{tricoloring}$ applied to $n$ and $h$ is a coloring of the cycle graph of $n$ and $\mathrm{Fin}$ applied to $3$.

SimpleGraph.pathGraph.bicoloringdefMathlib.Combinatorics.SimpleGraph.Coloring.Constructions, function or constant

Wording

no wording

English

Let $n$ be a natural number. Then $\operatorname{bicoloring}$ applied to $n$ is a coloring of the path graph of $n$ and $\mathrm{Bool}$.

SimpleGraph.pathGraph_two_embeddingdefMathlib.Combinatorics.SimpleGraph.Coloring.Constructions, function or constant

Wording

no wording

English

Let $n$ be a natural number such that $2 \leq n$. Then $\mathrm{SimpleGraph\_\_pathGraph\_two\_embedding}$ applied to $n$ and $h$ is an embedding of the path graph of $2$ and the path graph of $n$.

Mathlib.Combinatorics.SimpleGraph.Coloring.EdgeLabeling

SimpleGraph.EdgeLabelingdefMathlib.Combinatorics.SimpleGraph.Coloring.EdgeLabeling, type

Wording

edge labeling of G and K (from the name)

English

Let $G$ be a simple graph of $V$. Let $K$ be a set. Then an edge labeling of $G$ and $K$ is an element of the function that maps $G$ and $K$ to the set of functions from elements of the edge set for $G$ to elements of $K$.

SimpleGraph.EdgeLabeling.compRightdefMathlib.Combinatorics.SimpleGraph.Coloring.EdgeLabeling, function or constant

Wording

the right composition of C and f (from the name)

English

Let $C$ be an edge labeling of $G$ and $K$. Let $f$ be a function from elements of $K$ to elements of $\mathrm{K'}$. Then the right composition of $C$ and $f$ is an edge labeling of $G$ and $\mathrm{K'}$ defined as $\operatorname{comp}$ applied to $f$ and $C$.

SimpleGraph.EdgeLabeling.getdefMathlib.Combinatorics.SimpleGraph.Coloring.EdgeLabeling, function or constant

Wording

no wording

English

Let $C$ be an edge labeling of $G$ and $K$. Let $x$ and $y$ be elements of $V$ such that $\operatorname{Adj}$ holds for $G$, $x$ and $y$. Then $\operatorname{get}$ applied to $C$, $x$, $y$ and $h$ is an element of $K$ defined as $C$ applied to $\operatorname{mk}$ applied to $x$ and $y$.

SimpleGraph.EdgeLabeling.labelGraphdefMathlib.Combinatorics.SimpleGraph.Coloring.EdgeLabeling, function or constant

Wording

the label graph of C and k (from the name)

English

Let $C$ be an edge labeling of $G$ and $K$. Let $k$ be an element of $K$. Then the label graph of $C$ and $k$ is a simple graph of $V$ defined as $\operatorname{fromEdgeSet}$ applied to $\operatorname{ofPred}$ applied to the function that maps $e$ to the proposition that there exists an element $h$ of $\operatorname{mem}$ applied to $e$ and the edge set for $G$, such that $\EqtMACRoH {C (e)}{k}$.

SimpleGraph.EdgeLabeling.mkdefMathlib.Combinatorics.SimpleGraph.Coloring.EdgeLabeling, function or constant

Wording

no wording

English

Let $f$ be a function from elements $x_{1}$ of $V$ and elements $y_{1}$ of $V$ and elements of $\mathrm{Proof}$ applied to $\operatorname{Adj}$ applied to $G$, $x_{1}$ and $y_{1}$ to elements of $K$ such that for all elements $x$ and $y$ of $V$, for all elements $H$ of $\mathrm{Proof}$ applied to $\operatorname{Adj}$ applied to $G$, $x$ and $y$, $\EqtMACRoH {f (y , x , \operatorname{symm} (H))}{f (x , y , H)}$. Then there is an edge labeling of $G$ and $K$.

SimpleGraph.EdgeLabeling.pullbackdefMathlib.Combinatorics.SimpleGraph.Coloring.EdgeLabeling, function or constant

Wording

the pullback of C and f (from the name)

English

Let $C$ be an edge labeling of $G$ and $K$. Let $f$ be a homomorphism of $\mathrm{G'}$ and $G$. Then the pullback of $C$ and $f$ is an edge labeling of $\mathrm{G'}$ and $K$ defined as $\operatorname{comp}$ applied to $C$ and $\operatorname{mapEdgeSet}$ applied to $f$.

SimpleGraph.TopEdgeLabelingdefMathlib.Combinatorics.SimpleGraph.Coloring.EdgeLabeling, type

Wording

top edge labeling of V and K (from the name)

English

Let $V$ and $K$ be sets. Then a top edge labeling of $V$ and $K$ is an element of the function that maps $V$ and $K$ to the set of edge labelings of the top and $K$.

SimpleGraph.TopEdgeLabeling.pullbackdefMathlib.Combinatorics.SimpleGraph.Coloring.EdgeLabeling, function or constant

Wording

the pullback of C and f (from the name)

English

Let $C$ be a top edge labeling of $V$ and $K$. Let $f$ be an embedding of $\mathrm{V'}$ and $V$. Then the pullback of $C$ and $f$ is a top edge labeling of $\mathrm{V'}$ and $K$.

SimpleGraph.toTopEdgeLabelingdefMathlib.Combinatorics.SimpleGraph.Coloring.EdgeLabeling, function or constant

Wording

the top edge labeling of G (from the name)

English

Let $G$ be a simple graph of $V$. Then the top edge labeling of $G$ is a top edge labeling of $V$ and $\mathrm{Fin}$ applied to $2$.

Mathlib.Combinatorics.SimpleGraph.Coloring.Vertex

SimpleGraph.ColorabledefMathlib.Combinatorics.SimpleGraph.Coloring.Vertex, predicate

Wording

no wording

English

Let $G$ be a simple graph of $V$. Let $n$ be a natural number. Then $\operatorname{Colorable}$ holds for $G$ and $n$, if $\mathrm{Nonempty}$ holds for the set of colorings of $G$ and $\mathrm{Fin}$ applied to $n$.

SimpleGraph.Colorable.toColoringdefMathlib.Combinatorics.SimpleGraph.Coloring.Vertex, function or constant

Wording

the coloring of hc and hn (from the name)

English

Assume that $\operatorname{Colorable}$ holds for $G$ and $n$. Assume that $n$ is less than or equal to the cardinality of $x$. Then the coloring of $\mathrm{hc}$ and $\mathrm{hn}$ is a coloring of $G$ and $x$.

SimpleGraph.ColoringdefMathlib.Combinatorics.SimpleGraph.Coloring.Vertex, type

Wording

coloring of G and x (from the name)

English

Let $G$ be a simple graph of $V$. Let $x$ be a set. Then a coloring of $G$ and $x$ is an element of the function that maps $G$ and $x$ to the set of homomorphisms of $G$ and the complete graph of $x$.

SimpleGraph.Coloring.colorClassdefMathlib.Combinatorics.SimpleGraph.Coloring.Vertex, function or constant

Wording

the color class of C and c (from the docstring)

English

Let $C$ be a coloring of $G$ and $x$. Let $c$ be an element of $x$. Then the color class of $C$ and $c$ is an element of $\wp V$ defined as $\operatorname{ofPred}$ applied to the function that maps $v$ to $\EqtMACRoH {C (v)}{c}$.

SimpleGraph.Coloring.colorClassesdefMathlib.Combinatorics.SimpleGraph.Coloring.Vertex, function or constant

Wording

the color class of C (from the name)

English

Let $C$ be a coloring of $G$ and $x$. Then the color class of $C$ is an element of $\wp (\wp V)$ defined as the class of $\operatorname{ker}$ applied to $\operatorname{coe}$ applied to $C$.

SimpleGraph.Coloring.comapdefMathlib.Combinatorics.SimpleGraph.Coloring.Vertex, function or constant

Wording

the preimage of C and f (from the name)

English

Let $C$ be a coloring of $\mathrm{G'}$ and $x$. Let $f$ be a homomorphism of $G$ and $\mathrm{G'}$. Then the preimage of $C$ and $f$ is a coloring of $G$ and $x$ defined as the composition of $C$ and $f$.

SimpleGraph.Coloring.homMapdefMathlib.Combinatorics.SimpleGraph.Coloring.Vertex, function or constant

Wording

the homomorphism map of f (from the name)

English

Let $f$ be a coloring of $G$ and $x$. Then the homomorphism map of $f$ is a homomorphism of $G$ and the map of $\operatorname{coe}$ applied to $f$ and $G$.

SimpleGraph.Coloring.mkdefMathlib.Combinatorics.SimpleGraph.Coloring.Vertex, function or constant

Wording

no wording

English

Let $\mathrm{color}$ be a function from elements of $V$ to elements of $x$ such that for all elements $v$ and $w$ of $V$, if $\operatorname{Adj}$ holds for $G$, $v$ and $w$, then $\mathrm{color} (v)\neq \mathrm{color} (w)$. Then $\operatorname{mk}$ applied to $\mathrm{color}$ and $\mathrm{valid}$ is a coloring of $G$ and $x$ defined as $\operatorname{mk}$ applied to $\mathrm{color}$ and $\mathrm{valid}$.

SimpleGraph.Coloring.ofIsEmptydefMathlib.Combinatorics.SimpleGraph.Coloring.Vertex, function or constant

Wording

the coloring (from the docstring)

English

The coloring is a coloring of $G$ and $x$.

SimpleGraph.CompleteBipartiteGraph.bicoloringdefMathlib.Combinatorics.SimpleGraph.Coloring.Vertex, function or constant

Wording

no wording

English

Let $V$ and $W$ be sets. Then $\operatorname{bicoloring}$ applied to $V$ and $W$ is a coloring of the complete bipartite graph of $V$ and $W$ and $\mathrm{Bool}$.

SimpleGraph.chromaticNumberdefMathlib.Combinatorics.SimpleGraph.Coloring.Vertex, function or constant

Wording

the chromatic number of G (from the docstring)

English

Let $G$ be a simple graph of $V$. Then the chromatic number of $G$ is a natural number defined as the infimum of the function that maps $n$ to the infimum of the function that maps $h$ to $n$.

SimpleGraph.coloringCongrdefMathlib.Combinatorics.SimpleGraph.Coloring.Vertex, function or constant

Wording

the coloring congruence of f and g (from the name)

English

Let $f$ be an isomorphism of $G$ and $H$. Let $g$ be an equivalence from $x$ to $x_{1}$. Then the coloring congruence of $f$ and $g$ is an equivalence from the set of colorings of $G$ and $x$ to the set of colorings of $H$ and $x_{1}$ defined as the homomorphism congruence of $f$ and the complete graph of $g$.

SimpleGraph.completeMultipartiteGraph.coloringdefMathlib.Combinatorics.SimpleGraph.Coloring.Vertex, function or constant

Wording

the coloring of V (from the name)

English

Let $V$ be a function from elements of $x$ to sets. Then the coloring of $V$ is a coloring of the complete multipartite graph of $V$ and $x$.

SimpleGraph.recolorOfCardLEdefMathlib.Combinatorics.SimpleGraph.Coloring.Vertex, function or constant

Wording

no wording

English

Let $G$ be a simple graph of $V$. Assume that the cardinality of $x$ is less than or equal to the cardinality of $x_{1}$. Then $\operatorname{recolorOfCardLE}$ applied to $G$ and $\mathrm{hn}$ is an embedding of the set of colorings of $G$ and $x$ and the set of colorings of $G$ and $x_{1}$ defined as $\operatorname{recolorOfEmbedding}$ applied to $G$ and $\operatorname{some}$ applied to $\mathrm{Function\_\_Embedding\_\_nonempty\_of\_card\_le}$ applied to $\mathrm{hn}$.

SimpleGraph.recolorOfEmbeddingdefMathlib.Combinatorics.SimpleGraph.Coloring.Vertex, function or constant

Wording

no wording

English

Let $G$ be a simple graph of $V$. Let $f$ be an embedding of $x$ and $x_{1}$. Then $\operatorname{recolorOfEmbedding}$ applied to $G$ and $f$ is an embedding of the set of colorings of $G$ and $x$ and the set of colorings of $G$ and $x_{1}$.

SimpleGraph.recolorOfEquivdefMathlib.Combinatorics.SimpleGraph.Coloring.Vertex, function or constant

Wording

no wording

English

Let $G$ be a simple graph of $V$. Let $f$ be an equivalence from $x$ to $x_{1}$. Then $\operatorname{recolorOfEquiv}$ applied to $G$ and $f$ is an equivalence from the set of colorings of $G$ and $x$ to the set of colorings of $G$ and $x_{1}$.

SimpleGraph.selfColoringdefMathlib.Combinatorics.SimpleGraph.Coloring.Vertex, function or constant

Wording

the self coloring of G (from the name)

English

Let $G$ be a simple graph of $V$. Then the self coloring of $G$ is a coloring of $G$ and $V$ defined as $\operatorname{mk}$ applied to $\mathrm{id}$ and the function that maps $x$ and $x_{1}$ to $\mathrm{SimpleGraph\_\_ne\_of\_adj}$ applied to $G$.

Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite

SimpleGraph.CompleteEquipartiteSubgraphstructureMathlib.Combinatorics.SimpleGraph.CompleteMultipartite, type

Wording

complete equipartite subgraph of r and t (from the name)

English

Let $G$ be a simple graph of $V$. Let $r$ and $t$ be natural numbers. Then the complete equipartite subgraphs of $r$ and $t$ are a basic type.

SimpleGraph.CompleteEquipartiteSubgraph.ofCopydefMathlib.Combinatorics.SimpleGraph.CompleteMultipartite, function or constant

Wording

the complete equipartite subgraph of f (from the name)

English

Let $f$ be a copy of the complete equipartite graph of $r$ and $t$ and $G$. Then the complete equipartite subgraph of $f$ is a complete equipartite subgraph of $r$ and $t$.

SimpleGraph.CompleteEquipartiteSubgraph.partsdefMathlib.Combinatorics.SimpleGraph.CompleteMultipartite, function or constant

Wording

the parts of self (from the docstring)

English

Let $\mathrm{self}$ be a complete equipartite subgraph of $r$ and $t$. Then the parts of $\mathrm{self}$ is a finite set of the set of finite sets of $V$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.

SimpleGraph.CompleteEquipartiteSubgraph.toCopydefMathlib.Combinatorics.SimpleGraph.CompleteMultipartite, function or constant

Wording

the copy of K (from the name)

English

Let $K$ be a complete equipartite subgraph of $r$ and $t$. Then the copy of $K$ is a copy of the complete equipartite graph of $r$ and $t$ and $G$.

SimpleGraph.CompleteEquipartiteSubgraph.vertsdefMathlib.Combinatorics.SimpleGraph.CompleteMultipartite, function or constant

Wording

no wording

English

Let $K$ be a complete equipartite subgraph of $r$ and $t$. Then $\operatorname{verts}$ applied to $K$ is a finite set of $V$ defined as $\operatorname{disjiUnion}$ applied to the parts of $K$, $\mathrm{id}$ and $\operatorname{disjoint}$ applied to $K$.

SimpleGraph.IsCompleteMultipartitedefMathlib.Combinatorics.SimpleGraph.CompleteMultipartite, predicate

Wording

no wording

English

Let $G$ be a simple graph of $x$. Then $\operatorname{IsCompleteMultipartite}$ holds for $G$, if the function that maps $x_{1}$ and $x_{2}$ to the proposition that it is not the case that $\operatorname{Adj}$ holds for $G$, $x_{1}$ and $x_{2}$ is transitive.

SimpleGraph.IsCompleteMultipartite.isodefMathlib.Combinatorics.SimpleGraph.CompleteMultipartite, function or constant

Wording

the graph isomorphism of h (from the docstring)

English

Assume that $\operatorname{IsCompleteMultipartite}$ holds for $G$. Then the graph isomorphism of $h$ is an isomorphism of $G$ and the complete multipartite graph of the function that maps $c$ to $\SubtypeSet {x_{1}}{\operatorname{r} (\operatorname{out} (c), x_{1})}$.

SimpleGraph.IsPathGraph3ComplstructureMathlib.Combinatorics.SimpleGraph.CompleteMultipartite, predicate

Wording

no wording

English

Let $G$ be a simple graph of $x$. Let $v$, $x_{1}$ and $x_{2}$ be elements of $x$. Then we can say that $\operatorname{IsPathGraph3Compl}$ holds for $G$, $v$, $x_{1}$ and $x_{2}$.

SimpleGraph.IsPathGraph3Compl.pathGraph3ComplEmbeddingdefMathlib.Combinatorics.SimpleGraph.CompleteMultipartite, function or constant

Wording

the path graph complement embedding of h (from the name)

English

Assume that $\operatorname{IsPathGraph3Compl}$ holds for $G$, $v$, $x_{1}$ and $x_{2}$. Then the path graph complement embedding of $h$ is an embedding of the complement of the path graph of $3$ and $G$.

SimpleGraph.completeEquipartiteGraphdefMathlib.Combinatorics.SimpleGraph.CompleteMultipartite, function or constant

Wording

the complete equipartite graph of r and t (from the name)

English

Let $r$ and $t$ be natural numbers. Then the complete equipartite graph of $r$ and $t$ is a simple graph of $\mathrm{Prod}$ applied to $\mathrm{Fin}$ applied to $r$ and $\mathrm{Fin}$ applied to $t$ defined as the preimage of $\ProdfstMACRoZ$ and the top.

SimpleGraph.completeEquipartiteGraph.completeMultipartiteGraphdefMathlib.Combinatorics.SimpleGraph.CompleteMultipartite, function or constant

Wording

the complete multipartite graph (from the name)

English

The complete multipartite graph is an isomorphism of the complete equipartite graph of $r$ and $t$ and the complete multipartite graph of $\operatorname{const}$ applied to $\mathrm{Fin}$ applied to $r$ and $\mathrm{Fin}$ applied to $t$.

SimpleGraph.completeEquipartiteGraph.turanGraphdefMathlib.Combinatorics.SimpleGraph.CompleteMultipartite, function or constant

Wording

the Turan graph (from the name)

English

The Turan graph is an isomorphism of the complete equipartite graph of $r$ and $t$ and the Turan graph of $r \times t$ and $r$.

SimpleGraph.pathGraph3ComplEmbeddingOfdefMathlib.Combinatorics.SimpleGraph.CompleteMultipartite, function or constant

Wording

the path graph complement embedding of h (from the name)

English

Assume that it is not the case that $\operatorname{IsCompleteMultipartite}$ holds for $G$. Then the path graph complement embedding of $h$ is an embedding of the complement of the path graph of $3$ and $G$.

Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected

SimpleGraph.ConnectedstructureMathlib.Combinatorics.SimpleGraph.Connectivity.Connected, predicate

Wording

G is connected (from the docstring)

English

Let $G$ be a simple graph of $V$. Then we can say that $G$ is connected.

SimpleGraph.ConnectedComponentdefMathlib.Combinatorics.SimpleGraph.Connectivity.Connected, type

Wording

connected component of G (from the name)

English

Let $G$ be a simple graph of $V$. Then a connected component of $G$ is an element of the function that maps $G$ to $\mathrm{Quot}$ applied to $\operatorname{Reachable}$ applied to $G$.

SimpleGraph.ConnectedComponent.isoEquivSuppdefMathlib.Combinatorics.SimpleGraph.Connectivity.Connected, function or constant

Wording

the isomorphism equivalence support of x and C (from the name)

English

Let $x$ be an isomorphism of $G$ and $\mathrm{G'}$. Let $C$ be a connected component of $G$. Then the isomorphism equivalence support of $x$ and $C$ is an equivalence from the set of elements of the support of $C$ to the set of elements of the support of $\operatorname{connectedComponentEquiv}$ applied to $x$ and $C$.

SimpleGraph.ConnectedComponent.liftdefMathlib.Combinatorics.SimpleGraph.Connectivity.Connected, function or constant

Wording

the lift of f and x1 (from the name)

English

Let $f$ be a function from elements of $V$ to elements of $x$ such that for all elements $v$ and $w$ of $V$, for all walks $p$ of $v$ and $w$, if $p$ is a path, then $\EqtMACRoH {f (v)}{f (w)}$. Let $x_{1}$ be a connected component of $G$. Then the lift of $f$ and $x_{1}$ is an element of $x$.

SimpleGraph.ConnectedComponent.mapdefMathlib.Combinatorics.SimpleGraph.Connectivity.Connected, function or constant

Wording

the map of x and C (from the name)

English

Let $x$ be a homomorphism of $G$ and $\mathrm{G'}$. Let $C$ be a connected component of $G$. Then the map of $x$ and $C$ is a connected component of $\mathrm{G'}$.

SimpleGraph.ConnectedComponent.recOndefMathlib.Combinatorics.SimpleGraph.Connectivity.Connected, function or constant

Wording

no wording

English

Let $c$ be a connected component of $G$. Let $f$ be a function from elements $v_{1}$ of $V$ to elements of $\mathrm{motive}$ applied to the connected component of $G$ and $v_{1}$ such that for all elements $u$ and $v$ of $V$, for all walks $p$ of $u$ and $v$, if $p$ is a path, then $\EqtMACRoH {\operatorname{rec} (f (u), \operatorname{sound} (\operatorname{reachable} (p)))}{f (v)}$. Then $\operatorname{recOn}$ applied to $c$, $v_{1}$, $f$ and $h$ is an element of $\mathrm{motive}$ applied to $c$.

SimpleGraph.ConnectedComponent.suppdefMathlib.Combinatorics.SimpleGraph.Connectivity.Connected, function or constant

Wording

the support of C (from the name)

English

Let $C$ be a connected component of $G$. Then the support of $C$ is an element of $\wp V$ defined as $\operatorname{ofPred}$ applied to the function that maps $v$ to the proposition that the connected component of $G$ and $v$ is equal to $C$.

SimpleGraph.ConnectedComponent.toSimpleGraphdefMathlib.Combinatorics.SimpleGraph.Connectivity.Connected, function or constant

Wording

the simple graph of C (from the name)

English

Let $C$ be a connected component of $G$. Then the simple graph of $C$ is a simple graph of $\SubtypeSet {x}{(\MembershipmemMACRoT {C}{x})}$ defined as $\operatorname{induce}$ applied to the support of $C$ and $G$.

SimpleGraph.ConnectedComponent.toSimpleGraph_homdefMathlib.Combinatorics.SimpleGraph.Connectivity.Connected, function or constant

Wording

the simple graph homomorphism of C (from the name)

English

Let $C$ be a connected component of $G$. Then the simple graph homomorphism of $C$ is a homomorphism of the simple graph of $C$ and $G$.

SimpleGraph.IsBridgedefMathlib.Combinatorics.SimpleGraph.Connectivity.Connected, predicate

Wording

no wording

English

Let $G$ be a simple graph of $V$. Let $e$ be a symmetric square of $V$. Then $\operatorname{IsBridge}$ holds for $G$ and $e$, if $\operatorname{lift}$ holds for the function that maps $v$ and $w$ to the proposition that it is not the case that $\operatorname{Reachable}$ holds for $\operatorname{deleteEdges}$ applied to $G$ and $\operatorname{singleton}$ applied to $e$, $v$ and $w$ and $e$.

SimpleGraph.Iso.connectedComponentEquivdefMathlib.Combinatorics.SimpleGraph.Connectivity.Connected, function or constant

Wording

the connected component equivalence of x (from the name)

English

Let $x$ be an isomorphism of $G$ and $\mathrm{G'}$. Then the connected component equivalence of $x$ is an equivalence from the set of connected components of $G$ to the set of connected components of $\mathrm{G'}$.

SimpleGraph.PreconnecteddefMathlib.Combinatorics.SimpleGraph.Connectivity.Connected, predicate

Wording

G is preconnected (from the docstring)

English

Let $G$ be a simple graph of $V$. Then $G$ is preconnected, if for all elements $u$ and $v$ of $V$, $\operatorname{Reachable}$ holds for $G$, $u$ and $v$.

SimpleGraph.ReachabledefMathlib.Combinatorics.SimpleGraph.Connectivity.Connected, predicate

Wording

no wording

English

Let $G$ be a simple graph of $V$. Let $u$ and $v$ be elements of $V$. Then $\operatorname{Reachable}$ holds for $G$, $u$ and $v$, if $\mathrm{Nonempty}$ holds for the set of walks of $u$ and $v$.

SimpleGraph.connectedComponentMkdefMathlib.Combinatorics.SimpleGraph.Connectivity.Connected, function or constant

Wording

the connected component 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 connected component of $G$ and $v$ is a connected component of $G$ defined as $\operatorname{mk}$ applied to $\operatorname{Reachable}$ applied to $G$ and $v$.

SimpleGraph.edgeSetEquivSigmaConnectedComponentdefMathlib.Combinatorics.SimpleGraph.Connectivity.Connected, function or constant

Wording

the edge set equivalence sigma connected component of G (from the name)

English

Let $G$ be a simple graph of $V$. Then the edge set equivalence sigma connected component of $G$ is an equivalence from the set of elements of the edge set for $G$ to $\Sigma$ applied to the function that maps $c$ to the set of elements of the edge set for the simple graph of $c$ defined as the sigma quotient from relation of $\operatorname{symm}$ applied to $G$ and the relation homomorphism of the function that maps $x$ and $x_{1}$ to $\operatorname{reachable}$.

SimpleGraph.homOfConnectedComponentsdefMathlib.Combinatorics.SimpleGraph.Connectivity.Connected, function or constant

Wording

the homomorphism of G and C (from the name)

English

Let $G$ be a simple graph of $V$. Let $C$ be a function from connected components $c$ of $G$ to homomorphisms of the simple graph of $c$ and $H$. Then the homomorphism of $G$ and $c$ is a homomorphism of $G$ and $H$.

SimpleGraph.verticesEquivSigmaConnectedComponentdefMathlib.Combinatorics.SimpleGraph.Connectivity.Connected, function or constant

Wording

the vertice equivalence sigma connected component of G (from the name)

English

Let $G$ be a simple graph of $V$. Then the vertice equivalence sigma connected component of $G$ is an element of $\EquivMACRoAE {V}{\Sigma (\lambda c . \SubtypeSet {x}{(\MembershipmemMACRoT {c}{x})})}$ defined as the inverse of the sigma fiber equivalence of $\operatorname{connectedComponentMk}$ applied to $G$.

Mathlib.Combinatorics.SimpleGraph.Connectivity.EdgeConnectivity

SimpleGraph.IsEdgeConnecteddefMathlib.Combinatorics.SimpleGraph.Connectivity.EdgeConnectivity, predicate

Wording

no wording

English

Let $G$ be a simple graph of $V$. Let $k$ be a natural number. Then $\operatorname{IsEdgeConnected}$ holds for $G$ and $k$, if for all elements $u$ and $v$ of $V$, $\operatorname{IsEdgeReachable}$ holds for $G$, $k$, $u$ and $v$.

SimpleGraph.IsEdgeReachabledefMathlib.Combinatorics.SimpleGraph.Connectivity.EdgeConnectivity, predicate

Wording

no wording

English

Let $G$ be a simple graph of $V$. Let $k$ be a natural number. Let $u$ and $v$ be elements of $V$. Then $\operatorname{IsEdgeReachable}$ holds for $G$, $k$, $u$ and $v$, if for all elements $s$ of the power set of the set of symmetric squares of $V$, if the cardinality in $s$ is less than $k$, then $\operatorname{Reachable}$ holds for $\operatorname{deleteEdges}$ applied to $G$ and $s$, $u$ and $v$.

Mathlib.Combinatorics.SimpleGraph.Connectivity.Finite

SimpleGraph.oddComponentsdefMathlib.Combinatorics.SimpleGraph.Connectivity.Finite, function or constant

Wording

the odd component of G (from the name)

English

Let $G$ be a simple graph of $V$. Then the odd component of $G$ is an element of the power set of the set of connected components of $G$ defined as $\operatorname{ofPred}$ applied to the function that maps $c$ to the proposition that the cardinality of the support of $c$ is odd.

Mathlib.Combinatorics.SimpleGraph.Connectivity.Represents

SimpleGraph.ConnectedComponent.RepresentsdefMathlib.Combinatorics.SimpleGraph.Connectivity.Represents, predicate

Wording

no wording

English

Let $s$ be an element of $\wp V$. Let $C$ be an element of the power set of the set of connected components of $G$. Then $\operatorname{Represents}$ holds for $s$ and $C$, if $\operatorname{BijOn}$ holds for $\operatorname{connectedComponentMk}$ applied to $G$, $s$ and $C$.

Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph

SimpleGraph.ConnectedComponent.toSubgraphdefMathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph, function or constant

Wording

the induced subgraph of C (from the docstring)

English

Let $C$ be a connected component of $G$. Then the induced subgraph of $C$ is a subgraph of $G$ defined as the induced subgraph of the top and the support of $C$.

SimpleGraph.Subgraph.ConnectedstructureMathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph, predicate

Wording

H is connected (from the docstring)

English

Let $H$ be a subgraph of $G$. Then we can say that $H$ is connected.

SimpleGraph.Subgraph.PreconnectedstructureMathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph, predicate

Wording

H is preconnected (from the docstring)

English

Let $H$ be a subgraph of $G$. Then we can say that $H$ is preconnected.

SimpleGraph.Walk.mapToSubgraphdefMathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph, function or constant

Wording

the map to subgraph of w (from the name)

English

Let $w$ be a walk of $u$ and $v$. Then the map to subgraph of $w$ is a walk of $u$ and $v$ defined as $\operatorname{brecOn}$ applied to $w$ and $\mathrm{SimpleGraph\_\_Walk\_\_mapToSubgraph\_\_\_f}$.

SimpleGraph.Walk.toSubgraphdefMathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph, function or constant

Wording

the subgraph consisting of the vertices and edges of the walk of x (from the docstring)

English

Let $x$ be a walk of $u$ and $v$. Then the subgraph consisting of the vertices and edges of the walk of $x$ is a subgraph of $G$ defined as $\operatorname{brecOn}$ applied to $x$ and $\mathrm{SimpleGraph\_\_Walk\_\_toSubgraph\_\_\_f}$.

Mathlib.Combinatorics.SimpleGraph.Copy

SimpleGraph.CopystructureMathlib.Combinatorics.SimpleGraph.Copy, type

Wording

copy of H and G (from the name)

English

Let $H$ be a simple graph of $W$. Let $G$ be a simple graph of $V$. Then the copies of $H$ and $G$ are a basic type.

SimpleGraph.Copy.botdefMathlib.Combinatorics.SimpleGraph.Copy, function or constant

Wording

the bottom of f (from the name)

English

Let $f$ be an embedding of $W$ and $V$. Then the bottom of $f$ is a copy of the bottom and $G$.

SimpleGraph.Copy.compdefMathlib.Combinatorics.SimpleGraph.Copy, function or constant

Wording

the composition of g and f (from the name)

English

Let $g$ be a copy of $G$ and $I$. Let $f$ be a copy of $H$ and $G$. Then the composition of $g$ and $f$ is a copy of $H$ and $I$.

SimpleGraph.Copy.iddefMathlib.Combinatorics.SimpleGraph.Copy, function or constant

Wording

the identity copy of G (from the docstring)

English

Let $G$ be a simple graph of $V$. Then the identity copy of $G$ is a copy of $G$ and $G$ defined as $\operatorname{mk}$ applied to the identity homomorphism and $\mathrm{Function\_\_injective\_id}$.

SimpleGraph.Copy.inducedefMathlib.Combinatorics.SimpleGraph.Copy, function or constant

Wording

the copy of G and s (from the docstring)

English

Let $G$ be a simple graph of $V$. Let $s$ be an element of $\wp V$. Then the copy of $G$ and $s$ is a copy of $\operatorname{induce}$ applied to $s$ and $G$ and $G$ defined as the copy of $\operatorname{induce}$ applied to $s$.

SimpleGraph.Copy.isoSubgraphMapdefMathlib.Combinatorics.SimpleGraph.Copy, function or constant

Wording

the isomorphism subgraph map of f and #2 (from the name)

English

Let $f$ be a copy of $H$ and $G$. Let $\mathrm{A'}$ be a subgraph of $H$. Then the isomorphism subgraph map of $f$ and $\mathrm{A'}$ is an isomorphism of the coercion of $\mathrm{A'}$ and the coercion of the map of the homomorphism of $f$ and $\mathrm{A'}$.

SimpleGraph.Copy.isoToSubgraphdefMathlib.Combinatorics.SimpleGraph.Copy, function or constant

Wording

the isomorphism to subgraph of f (from the name)

English

Let $f$ be a copy of $H$ and $G$. Then the isomorphism to subgraph of $f$ is an isomorphism of $H$ and the coercion of the subgraph of $f$ defined as the composition of the isomorphism subgraph map of $f$ and the top and the inverse of the top isomorphism.

SimpleGraph.Copy.mapEdgeSetdefMathlib.Combinatorics.SimpleGraph.Copy, function or constant

Wording

the map edge set of f (from the name)

English

Let $f$ be a copy of $H$ and $G$. Then the map edge set of $f$ is an embedding of the set of elements of the edge set for $H$ and the set of elements of the edge set for $G$.

SimpleGraph.Copy.mapNeighborSetdefMathlib.Combinatorics.SimpleGraph.Copy, function or constant

Wording

the map neighbor set of f and a (from the name)

English

Let $f$ be a copy of $H$ and $G$. Let $a$ be an element of $W$. Then the map neighbor set of $f$ and $a$ is an embedding of the set of elements of the neighbor set of $H$ and $a$ and the set of elements of the neighbor set of $G$ and $f$ applied to $a$.

SimpleGraph.Copy.ofLEdefMathlib.Combinatorics.SimpleGraph.Copy, function or constant

Wording

the copy of x and x1 (from the name)

English

Let $x$ and $x_{1}$ be simple graphs of $V$ such that $x \leq x_{1}$. Then the copy of $x$ and $x_{1}$ is a copy of $x$ and $x_{1}$ defined as $\operatorname{mk}$ applied to the graph homomorphism of $h$ and $\mathrm{Function\_\_injective\_id}$.

SimpleGraph.Copy.toEmbeddingdefMathlib.Combinatorics.SimpleGraph.Copy, function or constant

Wording

the embedding of f (from the name)

English

Let $f$ be a copy of $H$ and $G$. Then the embedding of $f$ is an embedding of $W$ and $V$ defined as $\operatorname{mk}$ applied to $\operatorname{coe}$ applied to $f$ and $\operatorname{injective}$ applied to $f$.

SimpleGraph.Copy.toHomdefMathlib.Combinatorics.SimpleGraph.Copy, function or constant

Wording

the homomorphism of self (from the name)

English

Let $\mathrm{self}$ be a copy of $H$ and $G$. Then the homomorphism of $\mathrm{self}$ is a homomorphism of $H$ and $G$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.

SimpleGraph.Copy.toSubgraphdefMathlib.Combinatorics.SimpleGraph.Copy, function or constant

Wording

the subgraph of f (from the docstring)

English

Let $f$ be a copy of $H$ and $G$. Then the subgraph of $f$ is a subgraph of $G$ defined as the map of the homomorphism of $f$ and the top.

SimpleGraph.Copy.topEmbeddingdefMathlib.Combinatorics.SimpleGraph.Copy, function or constant

Wording

the top embedding of f (from the name)

English

Let $f$ be a copy of the top and $G$. Then the top embedding of $f$ is an embedding of the top and $G$.

SimpleGraph.Embedding.toCopydefMathlib.Combinatorics.SimpleGraph.Copy, function or constant

Wording

the copy of f (from the name)

English

Let $f$ be an embedding of $H$ and $G$. Then the copy of $f$ is a copy of $H$ and $G$.

SimpleGraph.FreedefMathlib.Combinatorics.SimpleGraph.Copy, predicate

Wording

no wording

English

Let $H$ be a simple graph of $W$. Let $G$ be a simple graph of $V$. Then $\operatorname{Free}$ holds for $H$ and $G$, if it is not the case that $\operatorname{IsContained}$ holds for $H$ and $G$.

SimpleGraph.Hom.toCopydefMathlib.Combinatorics.SimpleGraph.Copy, function or constant

Wording

the copy of f and h (from the name)

English

Let $f$ be a homomorphism of $H$ and $G$ such that $\operatorname{coe}$ applied to $f$ is injective. Then the copy of $f$ and $h$ is a copy of $H$ and $G$ defined as $\operatorname{mk}$ applied to $f$ and $h$.

SimpleGraph.IsContaineddefMathlib.Combinatorics.SimpleGraph.Copy, predicate

Wording

no wording

English

Let $H$ be a simple graph of $W$. Let $G$ be a simple graph of $V$. Then $\operatorname{IsContained}$ holds for $H$ and $G$, if $\mathrm{Nonempty}$ holds for the set of copies of $H$ and $G$.

SimpleGraph.IsIndContaineddefMathlib.Combinatorics.SimpleGraph.Copy, predicate

Wording

no wording

English

Let $G$ be a simple graph of $V$. Let $H$ be a simple graph of $W$. Then $\operatorname{IsIndContained}$ holds for $G$ and $H$, if $\mathrm{Nonempty}$ holds for the set of embeddings of $G$ and $H$.

SimpleGraph.Iso.toCopydefMathlib.Combinatorics.SimpleGraph.Copy, function or constant

Wording

the copy of f (from the name)

English

Let $f$ be an isomorphism of $H$ and $G$. Then the copy of $f$ is a copy of $H$ and $G$ defined as the copy of the embedding of $f$.

SimpleGraph.Subgraph.coeCopydefMathlib.Combinatorics.SimpleGraph.Copy, function or constant

Wording

the coercion copy of #1 (from the name)

English

Let $\mathrm{G'}$ be a subgraph of $G$. Then the coercion copy of $\mathrm{G'}$ is a copy of the coercion of $\mathrm{G'}$ and $G$ defined as the copy of the homomorphism of $\mathrm{G'}$ and $\mathrm{SimpleGraph\_\_Subgraph\_\_hom\_injective}$.

SimpleGraph.copyCountdefMathlib.Combinatorics.SimpleGraph.Copy, function or constant

Wording

the copy count 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 copy count of $G$ and $H$ is an element of $\Natural$ defined as $\FinsetcardMACRoM {(\FinsetFilter {\mathrm{G'}}{\mathrm{Nonempty} (\operatorname{Iso} (H , \operatorname{coe} (\mathrm{G'})))}{\FinsetunivMACRoAC})}$.

SimpleGraph.killCopiesdefMathlib.Combinatorics.SimpleGraph.Copy, function or constant

Wording

no wording

English

Let $G$ be a simple graph of $V$. Let $H$ be a simple graph of $W$. Then $\operatorname{killCopies}$ applied to $G$ and $H$ is a simple graph of $V$ defined as $\operatorname{proj0}$ applied to $\mathrm{SimpleGraph\_\_wrapped\_\_\_\_u40\_\_\_Mathlib\_\_Combinatorics\_\_SimpleGraph\_\_Copy\_\_3082331781\_\_\_hygCtx\_\_\_hyg\_\_14}$, $G$ and $H$.

SimpleGraph.labelledCopyCountdefMathlib.Combinatorics.SimpleGraph.Copy, function or constant

Wording

the labelled copy count 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 labelled copy count of $G$ and $H$ is a natural number defined as the cardinality of the set of copies of $H$ and $G$.

Mathlib.Combinatorics.SimpleGraph.CycleGraph

SimpleGraph.cycleGraphdefMathlib.Combinatorics.SimpleGraph.CycleGraph, function or constant

Wording

the cycle graph of n (from the name)

English

Let $n$ be a natural number. Then the cycle graph of $n$ is a simple graph of $\mathrm{Fin}$ applied to $n$.

SimpleGraph.cycleGraph.cycledefMathlib.Combinatorics.SimpleGraph.CycleGraph, function or constant

Wording

the Eulerian cycle of n (from the docstring)

English

Let $n$ be a natural number. Then the Eulerian cycle of $n$ is a walk of $0$ and $0$.

Mathlib.Combinatorics.SimpleGraph.Dart

SimpleGraph.DartstructureMathlib.Combinatorics.SimpleGraph.Dart, type

Wording

dart of G (from the name)

English

Let $G$ be a simple graph of $V$. Then the darts of $G$ are a basic type.

SimpleGraph.Dart.edgedefMathlib.Combinatorics.SimpleGraph.Dart, function or constant

Wording

the edge of d (from the name)

English

Let $d$ be a dart of $G$. Then the edge of $d$ is a symmetric square of $V$ defined as $\operatorname{mk}$ applied to $\ProdfstMACRoZ {\operatorname{toProd} (d)}$ and $\ProdsndMACRoAA {\operatorname{toProd} (d)}$.

SimpleGraph.Dart.symmdefMathlib.Combinatorics.SimpleGraph.Dart, function or constant

Wording

the inverse of d (from the name)

English

Let $d$ be a dart of $G$. Then the inverse of $d$ is a dart of $G$.

SimpleGraph.DartAdjdefMathlib.Combinatorics.SimpleGraph.Dart, predicate

Wording

no wording

English

Let $G$ be a simple graph of $V$. Let $d$ and $\mathrm{d'}$ be darts of $G$. Then $\operatorname{DartAdj}$ holds for $G$, $d$ and $\mathrm{d'}$, if $\EqtMACRoH {\ProdsndMACRoAA {\operatorname{toProd} (d)}}{\ProdfstMACRoZ {\operatorname{toProd} (\mathrm{d'})}}$.

SimpleGraph.dartOfNeighborSetdefMathlib.Combinatorics.SimpleGraph.Dart, function or constant

Wording

the dart of v and w (from the name)

English

Let $G$ be a simple graph of $V$. Let $v$ be an element of $V$. Let $w$ be an element of the neighbor set of $G$ and $v$. Then the dart of $v$ and $w$ is a dart of $G$.

Mathlib.Combinatorics.SimpleGraph.DeleteEdges

SimpleGraph.DeleteFardefMathlib.Combinatorics.SimpleGraph.DeleteEdges, predicate

Wording

no wording

English

Let $G$ be a simple graph of $V$. Let $p$ be a function from simple graphs of $V$ to propositions. Let $r$ be an element of $x$. Then $\operatorname{DeleteFar}$ holds for $G$, $p$ and $r$, if for all finite sets $s$ of the set of symmetric squares of $V$, if $s$ is less than or equal to the edge finite set of $G$, then if $p$ holds for $\operatorname{deleteEdges}$ applied to $G$ and $s$, then $r \leq \FinsetcardMACRoM {s}$.

SimpleGraph.deleteEdgesdefMathlib.Combinatorics.SimpleGraph.DeleteEdges, function or constant

Wording

no wording

English

Let $G$ be a simple graph of $V$. Let $s$ be an element of the power set of the set of symmetric squares of $V$. Then $\operatorname{deleteEdges}$ applied to $G$ and $s$ is a simple graph of $V$ defined as $\operatorname{sdiff}$ applied to $G$ and $\operatorname{fromEdgeSet}$ applied to $s$.

SimpleGraph.deleteIncidenceSetdefMathlib.Combinatorics.SimpleGraph.DeleteEdges, function or constant

Wording

no wording

English

Let $G$ be a simple graph of $V$. Let $x$ be an element of $V$. Then $\operatorname{deleteIncidenceSet}$ applied to $G$ and $x$ is a simple graph of $V$ defined as $\operatorname{deleteEdges}$ applied to $G$ and the incidence set of $G$ and $x$.

Mathlib.Combinatorics.SimpleGraph.Density

Rel.edgeDensitydefMathlib.Combinatorics.SimpleGraph.Density, function or constant

Wording

the edge density of s and t (from the name)

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 $t$ be a finite set of $x_{1}$. Then the edge density of $s$ and $t$ is a rational number defined as $\frac{ \FinsetcardMACRoM {\operatorname{interedges} (r , s , t)}}{\FinsetcardMACRoM {s}\times \FinsetcardMACRoM {t}}$.

Rel.interedgesdefMathlib.Combinatorics.SimpleGraph.Density, 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 $t$ be a finite set of $x_{1}$. Then $\operatorname{interedges}$ applied to $r$, $s$ and $t$ is a finite set of $\mathrm{Prod}$ applied to $x$ and $x_{1}$ defined as $\FinsetFilter {e}{r (\ProdfstMACRoZ {e}, \ProdsndMACRoAA {e})}{\operatorname{sprod} (s , t)}$.

SimpleGraph.edgeDensitydefMathlib.Combinatorics.SimpleGraph.Density, function or constant

Wording

the edge density of x2 and x3 (from the name)

English

Let $G$ be a simple graph of $x$. Let $x_{2}$ and $x_{3}$ be finite sets of $x$. Then the edge density of $x_{2}$ and $x_{3}$ is a rational number defined as the edge density of $x_{2}$ and $x_{3}$.

SimpleGraph.interedgesdefMathlib.Combinatorics.SimpleGraph.Density, function or constant

Wording

no wording

English

Let $G$ be a simple graph of $x$. Let $s$ and $t$ be finite sets of $x$. Then $\operatorname{interedges}$ applied to $G$, $s$ and $t$ is a finite set of $\mathrm{Prod}$ applied to $x$ and $x$ defined as $\operatorname{interedges}$ applied to $\operatorname{Adj}$ applied to $G$, $s$ and $t$.

Mathlib.Combinatorics.SimpleGraph.Diam

SimpleGraph.centerdefMathlib.Combinatorics.SimpleGraph.Diam, function or constant

Wording

the center of G (from the docstring)

English

Let $G$ be a simple graph of $x$. Then the center of $G$ is an element of $\wp x$ defined as $\operatorname{ofPred}$ applied to the function that maps $u$ to the proposition that the eccentricity of $G$ and $u$ is equal to the radius of $G$.

SimpleGraph.diamdefMathlib.Combinatorics.SimpleGraph.Diam, function or constant

Wording

the diameter of G (from the docstring)

English

Let $G$ be a simple graph of $x$. Then the diameter of $G$ is a natural number defined as the natural number of $\operatorname{ediam}$ applied to $G$.

SimpleGraph.eccentdefMathlib.Combinatorics.SimpleGraph.Diam, function or constant

Wording

the eccentricity of G and u (from the docstring)

English

Let $G$ be a simple graph of $x$. Let $u$ be an element of $x$. Then the eccentricity of $G$ and $u$ is a natural number defined as the supremum of the function that maps $v$ to the extended distance of $u$ and $v$.

SimpleGraph.ediamdefMathlib.Combinatorics.SimpleGraph.Diam, function or constant

Wording

no wording

English

Let $G$ be a simple graph of $x$. Then $\operatorname{ediam}$ applied to $G$ is a natural number defined as the supremum of the function that maps $u$ to the eccentricity of $G$ and $u$.

SimpleGraph.radiusdefMathlib.Combinatorics.SimpleGraph.Diam, function or constant

Wording

the radius of G (from the docstring)

English

Let $G$ be a simple graph of $x$. Then the radius of $G$ is a natural number defined as the infimum of the function that maps $u$ to the eccentricity of $G$ and $u$.

Mathlib.Combinatorics.SimpleGraph.Ends.Defs

SimpleGraph.ComponentCompldefMathlib.Combinatorics.SimpleGraph.Ends.Defs, type

Wording

component complement of G and K (from the name)

English

Let $G$ be a simple graph of $V$. Let $K$ be an element of $\wp V$. Then a component complement of $G$ and $K$ is an element of the function that maps $G$ and $K$ to the set of connected components of $\operatorname{induce}$ applied to the complement of $K$ and $G$.

SimpleGraph.ComponentCompl.coeGraphdefMathlib.Combinatorics.SimpleGraph.Ends.Defs, function or constant

Wording

the coercion graph of C (from the name)

English

Let $C$ be a component complement of $G$ and $K$. Then the coercion graph of $C$ is a simple graph of $\SubtypeSet {x}{(\MembershipmemMACRoT {C}{x})}$ defined as $\operatorname{induce}$ applied to $C$ and $G$.

SimpleGraph.ComponentCompl.homdefMathlib.Combinatorics.SimpleGraph.Ends.Defs, function or constant

Wording

the homomorphism of h and C (from the name)

English

Assume that $K \leq L$. Let $C$ be a component complement of $G$ and $L$. Then the homomorphism of $h$ and $C$ is a component complement of $G$ and $K$.

SimpleGraph.ComponentCompl.liftdefMathlib.Combinatorics.SimpleGraph.Ends.Defs, function or constant

Wording

the lift of f and h (from the name)

English

Let $f$ be a function from elements $v_{1}$ of $V$ and elements of $\mathrm{Proof}$ applied to the proposition that $v_{1}$ is not an element of $K$ to elements of $x$ such that for all elements $v$ and $w$ of $V$, for all elements $\mathrm{hv}$ of $\mathrm{Proof}$ applied to the proposition that $v$ is not an element of $K$, for all elements $\mathrm{hw}$ of $\mathrm{Proof}$ applied to the proposition that $w$ is not an element of $K$, if $\operatorname{Adj}$ holds for $G$, $v$ and $w$, then $\EqtMACRoH {f (v , \mathrm{hv})}{f (w , \mathrm{hw})}$. Let $x_{1}$ be a component complement of $G$ and $K$. Then the lift of $v_{1}$ and $h$ is an element of $x$.

SimpleGraph.ComponentCompl.suppdefMathlib.Combinatorics.SimpleGraph.Ends.Defs, function or constant

Wording

the support of C (from the name)

English

Let $C$ be a component complement of $G$ and $K$. Then the support of $C$ is an element of $\wp V$ defined as $\operatorname{ofPred}$ applied to the function that maps $v$ to the proposition that there exists an element $h$ of $\mathrm{not}$ applied to $\MembershipmemMACRoT {K}{v}$, such that the component complement of $G$ and $h$ is equal to $C$.

SimpleGraph.componentComplFunctordefMathlib.Combinatorics.SimpleGraph.Ends.Defs, function or constant

Wording

the component complement functor of G (from the name)

English

Let $G$ be a simple graph of $V$. Then the component complement functor of $G$ is a functor of the set of opposites of the set of finite sets of $V$ and the set of sets.

SimpleGraph.componentComplMkdefMathlib.Combinatorics.SimpleGraph.Ends.Defs, function or constant

Wording

the component complement of G and vK (from the name)

English

Let $G$ be a simple graph of $V$. Assume that $v$ is not an element of $K$. Then the component complement of $G$ and $\mathrm{vK}$ is a component complement of $G$ and $K$ defined as the connected component of $\operatorname{induce}$ applied to the complement of $K$ and $G$ and $v$.

SimpleGraph.enddefMathlib.Combinatorics.SimpleGraph.Ends.Defs, function or constant

Wording

the end of G (from the docstring)

English

Let $G$ be a simple graph of $V$. Then the end of $G$ is an element of the power set of the set of functions from opposites $j$ of the set of finite sets of $V$ to elements of the action of the component complement functor of $G$ and $j$ defined as the section of the component complement functor of $G$.

Mathlib.Combinatorics.SimpleGraph.Extremal.Basic

SimpleGraph.IsExtremaldefMathlib.Combinatorics.SimpleGraph.Extremal.Basic, predicate

Wording

no wording

English

Let $G$ be a simple graph of $V$. Let $p$ be a function from simple graphs of $V$ to propositions. Then $\operatorname{IsExtremal}$ holds for $G$ and $p$, if $p$ holds for $G$ and for all simple graphs $\mathrm{G'}$ of $V$, for all elements $x_{2}$ of $\mathrm{DecidableRel}$ applied to $\operatorname{Adj}$ applied to $\mathrm{G'}$, if $p$ holds for $\mathrm{G'}$, then the cardinality of the edge finite set of $\mathrm{G'}$ is less than or equal to the cardinality of the edge finite set of $G$.

SimpleGraph.extremalNumberdefMathlib.Combinatorics.SimpleGraph.Extremal.Basic, function or constant

Wording

the extremal number of n and H (from the docstring)

English

Let $n$ be a natural number. Let $H$ be a simple graph of $W$. Then the extremal number of $n$ and $H$ is a natural number defined as the supremum of $\FinsetFilter {G}{\operatorname{Free} (H , G)}{\FinsetunivMACRoAC}$ and the function that maps $x$ to the cardinality of the edge finite set of $x$.

Mathlib.Combinatorics.SimpleGraph.Extremal.Turan

SimpleGraph.IsTuranMaximaldefMathlib.Combinatorics.SimpleGraph.Extremal.Turan, predicate

Wording

no wording

English

Let $G$ be a simple graph of $V$. Let $r$ be a natural number. Then $\operatorname{IsTuranMaximal}$ holds for $G$ and $r$, if $\operatorname{IsExtremal}$ holds for $G$ and the function that maps $x_{2}$ to $\operatorname{CliqueFree}$ applied to $x_{2}$ and $r + 1$.

SimpleGraph.IsTuranMaximal.finpartitiondefMathlib.Combinatorics.SimpleGraph.Extremal.Turan, function or constant

Wording

the finpartition of h (from the name)

English

Assume that $\operatorname{IsTuranMaximal}$ holds for $G$ and $r$. Then the finpartition of $h$ is a finpartition of the universal set defined as the finpartition of $\operatorname{setoid}$ applied to $h$.

SimpleGraph.turanGraphdefMathlib.Combinatorics.SimpleGraph.Extremal.Turan, function or constant

Wording

the Turan graph of n and r (from the name)

English

Let $n$ and $r$ be natural numbers. Then the Turan graph of $n$ and $r$ is a simple graph of $\mathrm{Fin}$ applied to $n$.

SimpleGraph.turanNumberdefMathlib.Combinatorics.SimpleGraph.Extremal.Turan, function or constant

Wording

the Turan number of n and r (from the name)

English

Let $n$ and $r$ be natural numbers. Then the Turan number of $n$ and $r$ is a natural number defined as the cardinality of the edge finite set of the Turan graph of $n$ and $r$.

Mathlib.Combinatorics.SimpleGraph.Extremal.TuranDensity

SimpleGraph.turanDensitydefMathlib.Combinatorics.SimpleGraph.Extremal.TuranDensity, function or constant

Wording

the Turan density of H (from the name)

English

Let $H$ be a simple graph of $W$. Then the Turan density of $H$ is a real number defined as $\operatorname{limUnder}$ applied to $\operatorname{atTop}$ and the function that maps $n$ to the quotient of the extremal number of $n$ and $H$ and $\operatorname{choose}$ applied to $n$ and $2$.

SimpleGraph.turanDensityConstdefMathlib.Combinatorics.SimpleGraph.Extremal.TuranDensity, function or constant

Wording

the Turan density constant of H and x (from the name)

English

Let $H$ be a simple graph of $W$. Let $x$ be a real number. Then the Turan density constant of $H$ and $x$ is a natural number.

Mathlib.Combinatorics.SimpleGraph.Extremal.Zarankiewicz

SimpleGraph.zarankiewiczdefMathlib.Combinatorics.SimpleGraph.Extremal.Zarankiewicz, function or constant

Wording

no wording

English

Let $m$, $n$, $s$ and $t$ be elements of $\Natural$. Then $\operatorname{zarankiewicz}$ applied to $m$, $n$, $s$ and $t$ is an element of $\Natural$ defined as the supremum of $\FinsetFilter {G}{\mathrm{and} (\mathrm{Leq} (G , \mathrm{completeBipartiteGraph} (\mathrm{Fin} (m), \mathrm{Fin} (n))), \operatorname{Free} (\mathrm{completeBipartiteGraph} (\mathrm{Fin} (s), \mathrm{Fin} (t)), G))}{\FinsetunivMACRoAC}$ and the function that maps $x$ to $\FinsetcardMACRoM {\operatorname{edgeFinset} (x)}$.

Mathlib.Combinatorics.SimpleGraph.Finite

SimpleGraph.IsRegularOfDegreedefMathlib.Combinatorics.SimpleGraph.Finite, predicate

Wording

no wording

English

Let $G$ be a simple graph of $V$. Let $d$ be a natural number. Then $\operatorname{IsRegularOfDegree}$ holds for $G$ and $d$, if for all elements $v$ of $V$, the degree of $G$ and $v$ is equal to $d$.

SimpleGraph.LocallyFinitedefMathlib.Combinatorics.SimpleGraph.Finite, type

Wording

no wording

English

Let $G$ be a simple graph of $V$. Then an element of $\operatorname{LocallyFinite}$ applied to $G$ is an element of the function that maps $G$ to the set of functions from elements $v$ of $V$ to elements of $\mathrm{Fintype}$ applied to the set of elements of the neighbor set of $G$ and $v$.

SimpleGraph.degreedefMathlib.Combinatorics.SimpleGraph.Finite, function or constant

Wording

the degree 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 degree of $G$ and $v$ is a natural number defined as the cardinality of the neighbor finite set of $G$ and $v$.

SimpleGraph.edgeFinsetdefMathlib.Combinatorics.SimpleGraph.Finite, function or constant

Wording

the edge finite set of G (from the name)

English

Let $G$ be a simple graph of $V$. Then the edge finite set of $G$ is a finite set of the set of symmetric squares of $V$ defined as the finite set of the edge set for $G$.

SimpleGraph.incidenceFinsetdefMathlib.Combinatorics.SimpleGraph.Finite, function or constant

Wording

the incidence finite set 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 incidence finite set of $G$ and $v$ is a finite set of the set of symmetric squares of $V$ defined as the finite set of the incidence set of $G$ and $v$.

SimpleGraph.maxDegreedefMathlib.Combinatorics.SimpleGraph.Finite, function or constant

Wording

the maximum degree of G (from the name)

English

Let $G$ be a simple graph of $V$. Then the maximum degree of $G$ is a natural number defined as $\operatorname{unbotD}$ applied to $0$ and the maximum of the forward image of the universal set under the function that maps $v$ to the degree of $G$ and $v$.

SimpleGraph.minDegreedefMathlib.Combinatorics.SimpleGraph.Finite, function or constant

Wording

the minimum degree of G (from the name)

English

Let $G$ be a simple graph of $V$. Then the minimum degree of $G$ is a natural number defined as $\operatorname{untopD}$ applied to $0$ and the minimum of the forward image of the universal set under the function that maps $v$ to the degree of $G$ and $v$.

SimpleGraph.neighborFinsetdefMathlib.Combinatorics.SimpleGraph.Finite, function or constant

Wording

the neighbor finite set 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 neighbor finite set of $G$ and $v$ is a finite set of $V$ defined as the finite set of the neighbor set of $G$ and $v$.

Mathlib.Combinatorics.SimpleGraph.Finsubgraph

SimpleGraph.FinsubgraphdefMathlib.Combinatorics.SimpleGraph.Finsubgraph, type

Wording

no wording

English

Let $G$ be a simple graph of $V$. Then an element of $\operatorname{Finsubgraph}$ applied to $G$ is an element of the function that maps $G$ to $\SubtypeSet {\mathrm{G'}}{\operatorname{Finite} (\operatorname{verts} (\mathrm{G'}))}$.

SimpleGraph.FinsubgraphHomdefMathlib.Combinatorics.SimpleGraph.Finsubgraph, type

Wording

no wording

English

Let $\mathrm{G'}$ be an element of $\operatorname{Finsubgraph}$ applied to $G$. Let $F$ be a simple graph of $W$. Then an element of $\operatorname{FinsubgraphHom}$ applied to $\mathrm{G'}$ and $F$ is an element of the function that maps $\mathrm{G'}$ and $F$ to the set of homomorphisms of the coercion of $\mathrm{G'}$ and $F$.

SimpleGraph.FinsubgraphHom.restrictdefMathlib.Combinatorics.SimpleGraph.Finsubgraph, function or constant

Wording

no wording

English

Assume that $\mathrm{G''} \leq \mathrm{G'}$. Let $f$ be an element of $\operatorname{FinsubgraphHom}$ applied to $\mathrm{G'}$ and $F$. Then $\operatorname{restrict}$ applied to $h$ and $f$ is an element of $\operatorname{FinsubgraphHom}$ applied to $\mathrm{G''}$ and $F$.

SimpleGraph.finsubgraphHomFunctordefMathlib.Combinatorics.SimpleGraph.Finsubgraph, function or constant

Wording

no wording

English

Let $G$ be a simple graph of $V$. Let $F$ be a simple graph of $W$. Then $\operatorname{finsubgraphHomFunctor}$ applied to $G$ and $F$ is a functor of the set of opposites of $\operatorname{Finsubgraph}$ applied to $G$ and the set of sets.

SimpleGraph.finsubgraphOfAdjdefMathlib.Combinatorics.SimpleGraph.Finsubgraph, function or constant

Wording

no wording

English

Assume that $\operatorname{Adj}$ holds for $G$, $u$ and $v$. Then $\operatorname{finsubgraphOfAdj}$ applied to $e$ is an element of $\operatorname{Finsubgraph}$ applied to $G$ defined as the subgraph of $G$ and $e$.

SimpleGraph.singletonFinsubgraphdefMathlib.Combinatorics.SimpleGraph.Finsubgraph, function or constant

Wording

no wording

English

Let $v$ be an element of $V$. Then $\operatorname{singletonFinsubgraph}$ applied to $v$ is an element of $\operatorname{Finsubgraph}$ applied to $G$ defined as the singleton subgraph of $G$ and $v$.

Mathlib.Combinatorics.SimpleGraph.FiveWheelLike

SimpleGraph.FiveWheelLikeFreedefMathlib.Combinatorics.SimpleGraph.FiveWheelLike, predicate

Wording

no wording

English

Let $G$ be a simple graph of $x$. Let $r$ and $k$ be natural numbers. Then $\operatorname{FiveWheelLikeFree}$ holds for $G$, $r$ and $k$, if for all elements $v$, $x_{2}$ and $x_{3}$ of $x$, for all finite sets $s$ and $t$ of $x$, it is not the case that $\operatorname{IsFiveWheelLike}$ holds for $G$, $r$, $k$, $v$, $x_{2}$, $x_{3}$, $s$ and $t$.

SimpleGraph.IsFiveWheelLikestructureMathlib.Combinatorics.SimpleGraph.FiveWheelLike, predicate

Wording

no wording

English

Let $G$ be a simple graph of $x$. Let $r$ and $k$ be natural numbers. Let $v$, $x_{2}$ and $x_{3}$ be elements of $x$. Let $s$ and $t$ be finite sets of $x$. Then we can say that $\operatorname{IsFiveWheelLike}$ holds for $G$, $r$, $k$, $v$, $x_{2}$, $x_{3}$, $s$ and $t$.

Mathlib.Combinatorics.SimpleGraph.Girth

SimpleGraph.egirthdefMathlib.Combinatorics.SimpleGraph.Girth, function or constant

Wording

no wording

English

Let $G$ be a simple graph of $x$. Then $\operatorname{egirth}$ applied to $G$ is a natural number defined as the infimum of the function that maps $a$ to the infimum of the function that maps $w$ to the infimum of the function that maps $h$ to the length of $w$.

SimpleGraph.girthdefMathlib.Combinatorics.SimpleGraph.Girth, function or constant

Wording

the girth of G (from the docstring)

English

Let $G$ be a simple graph of $x$. Then the girth of $G$ is a natural number defined as the natural number of $\operatorname{egirth}$ applied to $G$.

Mathlib.Combinatorics.SimpleGraph.Hamiltonian

SimpleGraph.IsHamiltoniandefMathlib.Combinatorics.SimpleGraph.Hamiltonian, predicate

Wording

G is a Hamiltonian (from the name)

English

Let $G$ be a simple graph of $x$. Then $G$ is a Hamiltonian, if if the cardinality of $x$ is distinct from $1$, then there exists an element $a$ of $x$, such that there exists a walk $p$ of $a$ and $a$, such that $p$ is a Hamiltonian cycle.

SimpleGraph.Walk.IsHamiltoniandefMathlib.Combinatorics.SimpleGraph.Hamiltonian, predicate

Wording

p is a Hamiltonian (from the name)

English

Let $p$ be a walk of $a$ and $b$. Then $p$ is a Hamiltonian, if for all elements $a_{1}$ of $x$, the multiplicity of $a_{1}$ in the support of $p$ is equal to $1$.

SimpleGraph.Walk.IsHamiltonian.getVertEquivdefMathlib.Combinatorics.SimpleGraph.Hamiltonian, function or constant

Wording

no wording

English

Assume that $p$ is a Hamiltonian. Then $\operatorname{getVertEquiv}$ applied to $\mathrm{hp}$ is an equivalence from $\mathrm{Fin}$ applied to $\operatorname{length}$ applied to the support of $p$ to $x$.

SimpleGraph.Walk.IsHamiltonian.supportGetEquivdefMathlib.Combinatorics.SimpleGraph.Hamiltonian, function or constant

Wording

no wording

English

Assume that $p$ is a Hamiltonian. Then $\operatorname{supportGetEquiv}$ applied to $\mathrm{hp}$ is an equivalence from $\mathrm{Fin}$ applied to $\operatorname{length}$ applied to the support of $p$ to $x$ defined as $\operatorname{getEquivOfForallCountEqOne}$ applied to the support of $p$ and $\mathrm{hp}$.

SimpleGraph.Walk.IsHamiltonianCyclestructureMathlib.Combinatorics.SimpleGraph.Hamiltonian, predicate

Wording

p is a Hamiltonian cycle (from the name)

English

Let $p$ be a walk of $a$ and $a$. Then we can say that $p$ is a Hamiltonian cycle.

Mathlib.Combinatorics.SimpleGraph.Hasse

SimpleGraph.Walk.IsPath.pathGraphCopydefMathlib.Combinatorics.SimpleGraph.Hasse, function or constant

Wording

the path graph copy of hw (from the name)

English

Assume that $w$ is a path. Then the path graph copy of $\mathrm{hw}$ is a copy of the path graph of the sum of the length of $w$ and $1$ and $G$ defined as the composition of the coercion copy of the subgraph consisting of the vertices and edges of the walk of $w$ and the copy of the subgraph of $\mathrm{hw}$.

SimpleGraph.Walk.IsPath.pathGraphIsoToSubgraphdefMathlib.Combinatorics.SimpleGraph.Hasse, function or constant

Wording

the subgraph of hw (from the docstring)

English

Assume that $w$ is a path. Then the subgraph of $\mathrm{hw}$ is an isomorphism of the path graph of the sum of the length of $w$ and $1$ and the coercion of the subgraph consisting of the vertices and edges of the walk of $w$.

SimpleGraph.Walk.pathGraphHomdefMathlib.Combinatorics.SimpleGraph.Hasse, function or constant

Wording

the path graph homomorphism of w (from the name)

English

Let $w$ be a walk of $u$ and $v$. Then the path graph homomorphism of $w$ is a homomorphism of the path graph of the sum of the length of $w$ and $1$ and $G$ defined as the composition of the homomorphism of the subgraph consisting of the vertices and edges of the walk of $w$ and the subgraph of $w$.

SimpleGraph.Walk.pathGraphHomToSubgraphdefMathlib.Combinatorics.SimpleGraph.Hasse, function or constant

Wording

the subgraph of w (from the docstring)

English

Let $w$ be a walk of $u$ and $v$. Then the subgraph of $w$ is a homomorphism of the path graph of the sum of the length of $w$ and $1$ and the coercion of the subgraph consisting of the vertices and edges of the walk of $w$.

SimpleGraph.hassedefMathlib.Combinatorics.SimpleGraph.Hasse, function or constant

Wording

the Hasse diagram of x (from the docstring)

English

Let $x$ be a set. Then the Hasse diagram of $x$ is a simple graph of $x$.

SimpleGraph.hasseDualIsodefMathlib.Combinatorics.SimpleGraph.Hasse, function or constant

Wording

the Hasse dual isomorphism (from the name)

English

The Hasse dual isomorphism is an isomorphism of the Hasse diagram of the set of order duals of $x$ and the Hasse diagram of $x$.

SimpleGraph.pathGraphdefMathlib.Combinatorics.SimpleGraph.Hasse, function or constant

Wording

the path graph of n (from the name)

English

Let $n$ be a natural number. Then the path graph of $n$ is a simple graph of $\mathrm{Fin}$ applied to $n$ defined as the Hasse diagram of $\mathrm{Fin}$ applied to $n$.

Mathlib.Combinatorics.SimpleGraph.IncMatrix

SimpleGraph.incMatrixdefMathlib.Combinatorics.SimpleGraph.IncMatrix, function or constant

Wording

no wording

English

Let $R$ be a set. Let $G$ be a simple graph of $x$. Then there is a matrix of the set of symmetric squares of $x$ and $R$. Proof. Let $R$ be arbitrary. Let $G$ be arbitrary. Let $a_{1}$ be arbitrary. Let $e_{1}$ be arbitrary. By G. By a1. By SimpleGraph__incidenceSet. By e1. By Membership__mem. By 1. By 0. By ite. By Matrix__of__app.

Mathlib.Combinatorics.SimpleGraph.LapMatrix

SimpleGraph.degMatrixdefMathlib.Combinatorics.SimpleGraph.LapMatrix, function or constant

Wording

the degree matrix of R and G (from the name)

English

Let $R$ be a set. Let $G$ be a simple graph of $V$. Then the degree matrix of $R$ and $G$ is a matrix of $V$ and $R$ defined as the diagonal of the function that maps $x_{4}$ to the degree of $G$ and $x_{4}$.

SimpleGraph.lapMatrixdefMathlib.Combinatorics.SimpleGraph.LapMatrix, function or constant

Wording

no wording

English

Let $R$ be a set. Let $G$ be a simple graph of $V$. Then there is a matrix of $V$ and $R$. Proof. Let $R$ be arbitrary. Let $G$ be arbitrary. By R. By G. By SimpleGraph__degMatrix. By R. By G. By SimpleGraph__adjMatrix. By minus.

SimpleGraph.lapMatrix_ker_basisdefMathlib.Combinatorics.SimpleGraph.LapMatrix, function or constant

Wording

no wording

English

Let $G$ be a simple graph of $V$. Then $\mathrm{SimpleGraph\_\_lapMatrix\_ker\_basis}$ applied to $G$ is a basis of $\Real$ and $\SubtypeSet {x_{4}}{(\MembershipmemMACRoT {\operatorname{ker} (\operatorname{toLin'} (\operatorname{lapMatrix} (\Real , G)))}{x_{4}})}$ defined as $\operatorname{mk}$ applied to $\mathrm{SimpleGraph\_\_linearIndependent\_lapMatrix\_ker\_basis\_aux}$ applied to $G$ and $\mathrm{SimpleGraph\_\_top\_le\_span\_range\_lapMatrix\_ker\_basis\_aux}$ applied to $G$.

Mathlib.Combinatorics.SimpleGraph.LineGraph

SimpleGraph.Copy.lineGraphdefMathlib.Combinatorics.SimpleGraph.LineGraph, function or constant

Wording

the line graph of f (from the name)

English

Let $f$ be a copy of $G$ and $\mathrm{G'}$. Then the line graph of $f$ is a copy of the line graph of $G$ and the line graph of $\mathrm{G'}$ defined as the copy of the line graph embedding of $f$.

SimpleGraph.Copy.toLineGraphEmbeddingdefMathlib.Combinatorics.SimpleGraph.LineGraph, function or constant

Wording

the line graph embedding of f (from the name)

English

Let $f$ be a copy of $G$ and $\mathrm{G'}$. Then the line graph embedding of $f$ is an embedding of the line graph of $G$ and the line graph of $\mathrm{G'}$.

SimpleGraph.Iso.lineGraphdefMathlib.Combinatorics.SimpleGraph.LineGraph, function or constant

Wording

the line graph of f (from the name)

English

Let $f$ be an isomorphism of $G$ and $\mathrm{G'}$. Then the line graph of $f$ is an isomorphism of the line graph of $G$ and the line graph of $\mathrm{G'}$.

SimpleGraph.lineGraphdefMathlib.Combinatorics.SimpleGraph.LineGraph, function or constant

Wording

the line graph of G (from the docstring)

English

Let $G$ be a simple graph of $V$. Then the line graph of $G$ is a simple graph of the set of elements of the edge set for $G$.

Mathlib.Combinatorics.SimpleGraph.Maps

Equiv.simpleGraphdefMathlib.Combinatorics.SimpleGraph.Maps, function or constant

Wording

the simple graph of e (from the name)

English

Let $e$ be an equivalence from $V$ to $W$. Then the simple graph of $e$ is an equivalence from the set of simple graphs of $V$ to the set of simple graphs of $W$.

SimpleGraph.EmbeddingdefMathlib.Combinatorics.SimpleGraph.Maps, type

Wording

embedding of G and #2 (from the name)

English

Let $G$ be a simple graph of $V$. Let $\mathrm{G'}$ be a simple graph of $W$. Then an embedding of $G$ and $\mathrm{G'}$ is an element of the function that maps $G$ and $\mathrm{G'}$ to the set of relation embeddings of $\operatorname{Adj}$ applied to $G$ and $\operatorname{Adj}$ applied to $\mathrm{G'}$.

SimpleGraph.Embedding.comapdefMathlib.Combinatorics.SimpleGraph.Maps, function or constant

Wording

the preimage of f and G (from the name)

English

Let $f$ be an embedding of $V$ and $W$. Let $G$ be a simple graph of $W$. Then the preimage of $f$ and $G$ is an embedding of the preimage of $\operatorname{coe}$ applied to $f$ and $G$ and $G$.

SimpleGraph.Embedding.compdefMathlib.Combinatorics.SimpleGraph.Maps, function or constant

Wording

the composition of f and #2 (from the name)

English

Let $\mathrm{f'}$ be an embedding of $\mathrm{G'}$ and $\mathrm{G''}$. Let $f$ be an embedding of $G$ and $\mathrm{G'}$. Then the composition of $\mathrm{f'}$ and $f$ is an embedding of $G$ and $\mathrm{G''}$ defined as the composition of $f$ and $\mathrm{f'}$.

SimpleGraph.Embedding.complEquivdefMathlib.Combinatorics.SimpleGraph.Maps, function or constant

Wording

the complement equivalence (from the name)

English

The complement equivalence is an equivalence from the set of embeddings of $G$ and $H$ to the set of embeddings of the complement of $G$ and the complement of $H$.

SimpleGraph.Embedding.completeGraphdefMathlib.Combinatorics.SimpleGraph.Maps, function or constant

Wording

the complete graph of f (from the name)

English

Let $f$ be an embedding of $x$ and $x_{1}$. Then the complete graph of $f$ is an embedding of the complete graph of $x$ and the complete graph of $x_{1}$.

SimpleGraph.Embedding.inducedefMathlib.Combinatorics.SimpleGraph.Maps, function or constant

Wording

no wording

English

Let $s$ be an element of $\wp V$. Then $\operatorname{induce}$ applied to $s$ is an embedding of $\operatorname{induce}$ applied to $s$ and $G$ and $G$ defined as the preimage of the subtype of the function that maps $x$ to $\MembershipmemMACRoT {s}{x}$ and $G$.

SimpleGraph.Embedding.isoInduceRangedefMathlib.Combinatorics.SimpleGraph.Maps, function or constant

Wording

no wording

English

Let $f$ be an embedding of $G$ and $\mathrm{G'}$. Then $\operatorname{isoInduceRange}$ applied to $f$ is an isomorphism of $G$ and $\operatorname{induce}$ applied to the range of $\operatorname{coe}$ applied to $f$ and $\mathrm{G'}$.

SimpleGraph.Embedding.mapdefMathlib.Combinatorics.SimpleGraph.Maps, function or constant

Wording

the map of f and G (from the name)

English

Let $f$ be an embedding of $V$ and $W$. Let $G$ be a simple graph of $V$. Then the map of $f$ and $G$ is an embedding of $G$ and the map of $\operatorname{coe}$ applied to $f$ and $G$.

SimpleGraph.Embedding.mapEdgeSetdefMathlib.Combinatorics.SimpleGraph.Maps, function or constant

Wording

the map edge set of f (from the name)

English

Let $f$ be an embedding of $G$ and $\mathrm{G'}$. Then the map edge set of $f$ is an embedding of the set of elements of the edge set for $G$ and the set of elements of the edge set for $\mathrm{G'}$.

SimpleGraph.Embedding.mapNeighborSetdefMathlib.Combinatorics.SimpleGraph.Maps, function or constant

Wording

the map neighbor set of f and v (from the name)

English

Let $f$ be an embedding of $G$ and $\mathrm{G'}$. Let $v$ be an element of $V$. Then the map neighbor set of $f$ and $v$ is an embedding of the set of elements of the neighbor set of $G$ and $v$ and the set of elements of the neighbor set of $\mathrm{G'}$ and $f$ applied to $v$.

SimpleGraph.Embedding.refldefMathlib.Combinatorics.SimpleGraph.Maps, function or constant

Wording

the identity embedding (from the docstring)

English

The identity embedding is an embedding of $G$ and $G$ defined as the identity of $\operatorname{Adj}$ applied to $G$.

SimpleGraph.Embedding.spanningCoedefMathlib.Combinatorics.SimpleGraph.Maps, function or constant

Wording

the spanning coercion of G (from the name)

English

Let $G$ be a simple graph of the set of elements of $s$. Then the spanning coercion of $G$ is an embedding of $G$ and the spanning coercion of $G$ defined as the map of the subtype of the function that maps $x$ to $\MembershipmemMACRoT {s}{x}$ and $G$.

SimpleGraph.Embedding.toHomdefMathlib.Combinatorics.SimpleGraph.Maps, function or constant

Wording

the homomorphism of f (from the name)

English

Let $f$ be an embedding of $G$ and $\mathrm{G'}$. Then the homomorphism of $f$ is a homomorphism of $G$ and $\mathrm{G'}$ defined as the relation homomorphism of $f$.

SimpleGraph.HomdefMathlib.Combinatorics.SimpleGraph.Maps, type

Wording

homomorphism of G and #2 (from the name)

English

Let $G$ be a simple graph of $V$. Let $\mathrm{G'}$ be a simple graph of $W$. Then a homomorphism of $G$ and $\mathrm{G'}$ is an element of the function that maps $G$ and $\mathrm{G'}$ to the set of relation homomorphisms of $\operatorname{Adj}$ applied to $G$ and $\operatorname{Adj}$ applied to $\mathrm{G'}$.

SimpleGraph.Hom.comapdefMathlib.Combinatorics.SimpleGraph.Maps, function or constant

Wording

the preimage of f and G (from the name)

English

Let $f$ be a function from elements of $V$ to elements of $W$. Let $G$ be a simple graph of $W$. Then the preimage of $f$ and $G$ is a homomorphism of the preimage of $f$ and $G$ and $G$.

SimpleGraph.Hom.compdefMathlib.Combinatorics.SimpleGraph.Maps, function or constant

Wording

the composition of f and #2 (from the name)

English

Let $\mathrm{f'}$ be a homomorphism of $\mathrm{G'}$ and $\mathrm{G''}$. Let $f$ be a homomorphism of $G$ and $\mathrm{G'}$. Then the composition of $\mathrm{f'}$ and $f$ is a homomorphism of $G$ and $\mathrm{G''}$ defined as the composition of $\mathrm{f'}$ and $f$.

SimpleGraph.Hom.iddefMathlib.Combinatorics.SimpleGraph.Maps, function or constant

Wording

the identity homomorphism (from the docstring)

English

The identity homomorphism is a homomorphism of $G$ and $G$ defined as the identity of $\operatorname{Adj}$ applied to $G$.

SimpleGraph.Hom.mapdefMathlib.Combinatorics.SimpleGraph.Maps, function or constant

Wording

the map of f and G (from the name)

English

Let $f$ be a function from elements of $V$ to elements of $W$. Let $G$ be a simple graph of $V$ such that for all elements $u$ and $v$ of $V$, if $\operatorname{Adj}$ holds for $G$, $u$ and $v$, then $f (u)\neq f (v)$. Then the map of $f$ and $G$ is a homomorphism of $G$ and the map of $f$ and $G$.

SimpleGraph.Hom.mapDartdefMathlib.Combinatorics.SimpleGraph.Maps, function or constant

Wording

the map dart of f and d (from the name)

English

Let $f$ be a homomorphism of $G$ and $\mathrm{G'}$. Let $d$ be a dart of $G$. Then the map dart of $f$ and $d$ is a dart of $\mathrm{G'}$.

SimpleGraph.Hom.mapEdgeSetdefMathlib.Combinatorics.SimpleGraph.Maps, function or constant

Wording

the map edge set of f and e (from the name)

English

Let $f$ be a homomorphism of $G$ and $\mathrm{G'}$. Let $e$ be an element of the edge set for $G$. Then the map edge set of $f$ and $e$ is an element of the edge set for $\mathrm{G'}$ defined as the map of $\operatorname{coe}$ applied to $f$ and $e$.

SimpleGraph.Hom.mapNeighborSetdefMathlib.Combinatorics.SimpleGraph.Maps, function or constant

Wording

the map neighbor set of v and w (from the name)

English

Let $f$ be a homomorphism of $G$ and $\mathrm{G'}$. Let $v$ be an element of $V$. Let $w$ be an element of the neighbor set of $G$ and $v$. Then the map neighbor set of $v$ and $w$ is an element of the neighbor set of $\mathrm{G'}$ and $f$ applied to $v$ defined as $f$ applied to $w$.

SimpleGraph.Hom.ofLEdefMathlib.Combinatorics.SimpleGraph.Maps, function or constant

Wording

the graph homomorphism of h (from the docstring)

English

Assume that $x \leq x_{1}$. Then the graph homomorphism of $h$ is a homomorphism of $x$ and $x_{1}$ defined as $\operatorname{mk}$ applied to $\mathrm{id}$ and $h$.

SimpleGraph.HomClassdefMathlib.Combinatorics.SimpleGraph.Maps, predicate

Wording

no wording

English

Let $F$ be a set. Let $G$ be a simple graph of $V$. Let $H$ be a simple graph of $W$. Then $\operatorname{HomClass}$ holds for $F$, $G$ and $H$, if $\mathrm{RelHomClass}$ holds for $F$, $\operatorname{Adj}$ applied to $G$ and $\operatorname{Adj}$ applied to $H$.

SimpleGraph.IsodefMathlib.Combinatorics.SimpleGraph.Maps, type

Wording

isomorphism of G and #2 (from the name)

English

Let $G$ be a simple graph of $V$. Let $\mathrm{G'}$ be a simple graph of $W$. Then an isomorphism of $G$ and $\mathrm{G'}$ is an element of the function that maps $G$ and $\mathrm{G'}$ to the set of relation isomorphisms of $\operatorname{Adj}$ applied to $G$ and $\operatorname{Adj}$ applied to $\mathrm{G'}$.

SimpleGraph.Iso.comapdefMathlib.Combinatorics.SimpleGraph.Maps, function or constant

Wording

the preimage of f and G (from the name)

English

Let $f$ be an equivalence from $V$ to $W$. Let $G$ be a simple graph of $W$. Then the preimage of $f$ and $G$ is an isomorphism of the preimage of $\operatorname{coe}$ applied to $f$ and $G$ and $G$.

SimpleGraph.Iso.compdefMathlib.Combinatorics.SimpleGraph.Maps, function or constant

Wording

the composition of f and #2 (from the name)

English

Let $\mathrm{f'}$ be an isomorphism of $\mathrm{G'}$ and $\mathrm{G''}$. Let $f$ be an isomorphism of $G$ and $\mathrm{G'}$. Then the composition of $\mathrm{f'}$ and $f$ is an isomorphism of $G$ and $\mathrm{G''}$ defined as the composition of $f$ and $\mathrm{f'}$.

SimpleGraph.Iso.completeGraphdefMathlib.Combinatorics.SimpleGraph.Maps, function or constant

Wording

the complete graph of f (from the name)

English

Let $f$ be an equivalence from $x$ to $x_{1}$. Then the complete graph of $f$ is an isomorphism of the complete graph of $x$ and the complete graph of $x_{1}$.

SimpleGraph.Iso.homCongrdefMathlib.Combinatorics.SimpleGraph.Maps, function or constant

Wording

the homomorphism congruence of f and #2 (from the name)

English

Let $f$ be an isomorphism of $G$ and $\mathrm{G'}$. Let $\mathrm{f'}$ be an isomorphism of $\mathrm{G''}$ and $\mathrm{G'''}$. Then the homomorphism congruence of $f$ and $\mathrm{f'}$ is an equivalence from the set of homomorphisms of $G$ and $\mathrm{G''}$ to the set of homomorphisms of $\mathrm{G'}$ and $\mathrm{G'''}$ defined as the relation homomorphism congruence of $f$ and $\mathrm{f'}$.

SimpleGraph.Iso.inducedefMathlib.Combinatorics.SimpleGraph.Maps, function or constant

Wording

the restriction of x and h (from the docstring)

English

Let $x$ be an isomorphism of $G$ and $\mathrm{G'}$ such that $\operatorname{BijOn}$ holds for $\operatorname{coe}$ applied to $x$, $s$ and $t$. Then the restriction of $x$ and $h$ is an isomorphism of $\operatorname{induce}$ applied to $s$ and $G$ and $\operatorname{induce}$ applied to $t$ and $\mathrm{G'}$.

SimpleGraph.Iso.mapdefMathlib.Combinatorics.SimpleGraph.Maps, function or constant

Wording

the map of f and G (from the name)

English

Let $f$ be an equivalence from $V$ to $W$. Let $G$ be a simple graph of $V$. Then the map of $f$ and $G$ is an isomorphism of $G$ and the map of $\operatorname{coe}$ applied to $f$ and $G$.

SimpleGraph.Iso.mapEdgeSetdefMathlib.Combinatorics.SimpleGraph.Maps, function or constant

Wording

the map edge set of f (from the name)

English

Let $f$ be an isomorphism of $G$ and $\mathrm{G'}$. Then the map edge set of $f$ is an equivalence from the set of elements of the edge set for $G$ to the set of elements of the edge set for $\mathrm{G'}$.

SimpleGraph.Iso.mapNeighborSetdefMathlib.Combinatorics.SimpleGraph.Maps, function or constant

Wording

the map neighbor set of f and v (from the name)

English

Let $f$ be an isomorphism of $G$ and $\mathrm{G'}$. Let $v$ be an element of $V$. Then the map neighbor set of $f$ and $v$ is an equivalence from the set of elements of the neighbor set of $G$ and $v$ to the set of elements of the neighbor set of $\mathrm{G'}$ and $f$ applied to $v$.

SimpleGraph.Iso.refldefMathlib.Combinatorics.SimpleGraph.Maps, function or constant

Wording

the identity isomorphism (from the docstring)

English

The identity isomorphism is an isomorphism of $G$ and $G$ defined as the identity of $\operatorname{Adj}$ applied to $G$.

SimpleGraph.Iso.symmdefMathlib.Combinatorics.SimpleGraph.Maps, function or constant

Wording

the inverse of f (from the docstring)

English

Let $f$ be an isomorphism of $G$ and $\mathrm{G'}$. Then the inverse of $f$ is an isomorphism of $\mathrm{G'}$ and $G$ defined as the inverse of $f$.

SimpleGraph.Iso.toEmbeddingdefMathlib.Combinatorics.SimpleGraph.Maps, function or constant

Wording

the embedding of f (from the name)

English

Let $f$ be an isomorphism of $G$ and $\mathrm{G'}$. Then the embedding of $f$ is an embedding of $G$ and $\mathrm{G'}$ defined as the relation embedding of $f$.

SimpleGraph.Iso.toHomdefMathlib.Combinatorics.SimpleGraph.Maps, function or constant

Wording

the homomorphism of f (from the name)

English

Let $f$ be an isomorphism of $G$ and $\mathrm{G'}$. Then the homomorphism of $f$ is a homomorphism of $G$ and $\mathrm{G'}$ defined as the homomorphism of the embedding of $f$.

SimpleGraph.comapdefMathlib.Combinatorics.SimpleGraph.Maps, function or constant

Wording

the preimage of f and G (from the name)

English

Let $f$ be a function from elements of $V$ to elements of $W$. Let $G$ be a simple graph of $W$. Then the preimage of $f$ and $G$ is a simple graph of $V$.

SimpleGraph.completeBipartiteGraphCongrdefMathlib.Combinatorics.SimpleGraph.Maps, function or constant

Wording

the complete bipartite graph congruence of hV and hW (from the name)

English

Let $\mathrm{hV}$ be an equivalence from $x$ to $x_{1}$. Let $\mathrm{hW}$ be an equivalence from $x_{2}$ to $x_{3}$. Then the complete bipartite graph congruence of $\mathrm{hV}$ and $\mathrm{hW}$ is an isomorphism of the complete bipartite graph of $x$ and $x_{2}$ and the complete bipartite graph of $x_{1}$ and $x_{3}$.

SimpleGraph.completeMultipartiteGraphdefMathlib.Combinatorics.SimpleGraph.Maps, function or constant

Wording

the complete multipartite graph of V (from the name)

English

Let $V$ be a function from elements of $x$ to sets. Then the complete multipartite graph of $V$ is a simple graph of $\Sigma$ applied to the function that maps $i$ to $V$ applied to $i$ defined as the preimage of $\operatorname{fst}$ and the top.

SimpleGraph.inducedefMathlib.Combinatorics.SimpleGraph.Maps, function or constant

Wording

no wording

English

Let $s$ be an element of $\wp V$. Let $G$ be a simple graph of $V$. Then $\operatorname{induce}$ applied to $s$ and $G$ is a simple graph of the set of elements of $s$ defined as the preimage of $\operatorname{coe}$ applied to the subtype of the function that maps $x$ to $\MembershipmemMACRoT {s}{x}$ and $G$.

SimpleGraph.induceHomdefMathlib.Combinatorics.SimpleGraph.Maps, function or constant

Wording

the restriction of x and h (from the docstring)

English

Let $x$ be a homomorphism of $G$ and $\mathrm{G'}$ such that $\operatorname{MapsTo}$ holds for $\operatorname{coe}$ applied to $x$, $s$ and $t$. Then the restriction of $x$ and $h$ is a homomorphism of $\operatorname{induce}$ applied to $s$ and $G$ and $\operatorname{induce}$ applied to $t$ and $\mathrm{G'}$.

SimpleGraph.induceHomOfLEdefMathlib.Combinatorics.SimpleGraph.Maps, function or constant

Wording

no wording

English

Let $G$ be a simple graph of $V$. Assume that $s \leq \mathrm{s'}$. Then $\operatorname{induceHomOfLE}$ applied to $G$ and $h$ is an embedding of $\operatorname{induce}$ applied to $s$ and $G$ and $\operatorname{induce}$ applied to $\mathrm{s'}$ and $G$.

SimpleGraph.induceUnivIsodefMathlib.Combinatorics.SimpleGraph.Maps, function or constant

Wording

no wording

English

Let $G$ be a simple graph of $V$. Then $\operatorname{induceUnivIso}$ applied to $G$ is an isomorphism of $\operatorname{induce}$ applied to the universal set and $G$ and $G$.

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

Wording

the map of f and G (from the name)

English

Let $f$ be a function from elements of $V$ to elements of $W$. Let $G$ be a simple graph of $V$. Then the map of $f$ and $G$ is a simple graph of $W$.

SimpleGraph.overFindefMathlib.Combinatorics.SimpleGraph.Maps, function or constant

Wording

no wording

English

Let $G$ be a simple graph of $V$. Assume that the cardinality of $V$ is equal to $n$. Then $\operatorname{overFin}$ applied to $G$ and $\mathrm{hc}$ is a simple graph of $\mathrm{Fin}$ applied to $n$ defined as the preimage of $\operatorname{coe}$ applied to the inverse of $\operatorname{equivFinOfCardEq}$ applied to $\mathrm{hc}$ and $G$.

SimpleGraph.overFinIsodefMathlib.Combinatorics.SimpleGraph.Maps, function or constant

Wording

no wording

English

Let $G$ be a simple graph of $V$. Assume that the cardinality of $V$ is equal to $n$. Then $\operatorname{overFinIso}$ applied to $G$ and $\mathrm{hc}$ is an isomorphism of $G$ and $\operatorname{overFin}$ applied to $G$ and $\mathrm{hc}$ defined as the inverse of the preimage of the inverse of $\operatorname{equivFinOfCardEq}$ applied to $\mathrm{hc}$ and $G$.

SimpleGraph.spanningCoedefMathlib.Combinatorics.SimpleGraph.Maps, function or constant

Wording

the spanning coercion of G (from the name)

English

Let $G$ be a simple graph of the set of elements of $s$. Then the spanning coercion of $G$ is a simple graph of $V$ defined as the map of $\operatorname{coe}$ applied to the subtype of the function that maps $x$ to $\MembershipmemMACRoT {s}{x}$ and $G$.

Mathlib.Combinatorics.SimpleGraph.Matching

SimpleGraph.IsAlternatingdefMathlib.Combinatorics.SimpleGraph.Matching, predicate

Wording

no wording

English

Let $G$ and $\mathrm{G'}$ be simple graphs of $V$. Then $\operatorname{IsAlternating}$ holds for $G$ and $\mathrm{G'}$, if for all elements $v$, $w$ and $\mathrm{w'}$ of $V$, if $w \neq \mathrm{w'}$, then if $\operatorname{Adj}$ holds for $G$, $v$ and $w$, then if $\operatorname{Adj}$ holds for $G$, $v$ and $\mathrm{w'}$, then $\operatorname{Adj}$ holds for $\mathrm{G'}$, $v$ and $w$, if and only if it is not the case that $\operatorname{Adj}$ holds for $\mathrm{G'}$, $v$ and $\mathrm{w'}$.

SimpleGraph.IsCyclesdefMathlib.Combinatorics.SimpleGraph.Matching, predicate

Wording

no wording

English

Let $G$ be a simple graph of $V$. Then $\operatorname{IsCycles}$ holds for $G$, if for all elements $v$ of $V$, if the neighbor set of $G$ and $v$ is nonempty, then the cardinality of the neighbor set of $G$ and $v$ is equal to $2$.

SimpleGraph.IsMatchingFreedefMathlib.Combinatorics.SimpleGraph.Matching, predicate

Wording

G is a matching free (from the name)

English

Let $G$ be a simple graph of $V$. Then $G$ is a matching free, if for all subgraphs $M$ of $G$, $M$ is not a perfect matching.

SimpleGraph.Subgraph.IsMatchingdefMathlib.Combinatorics.SimpleGraph.Matching, predicate

Wording

M is a matching (from the name)

English

Let $M$ be a subgraph of $G$. Then $M$ is a matching, if for all elements $v$ of $V$, if $\MembershipmemMACRoT {\operatorname{verts} (M)}{v}$, then $\mathrm{ExistsUnique}$ holds for the function that maps $w$ to $\operatorname{Adj}$ applied to $M$, $v$ and $w$.

SimpleGraph.Subgraph.IsMatching.toEdgedefMathlib.Combinatorics.SimpleGraph.Matching, function or constant

Wording

the edge of h and v (from the name)

English

Assume that $M$ is a matching. Let $v$ be an element of $\operatorname{verts}$ applied to $M$. Then the edge of $h$ and $v$ is an element of the edge set of $M$.

SimpleGraph.Subgraph.IsPerfectMatchingdefMathlib.Combinatorics.SimpleGraph.Matching, predicate

Wording

M is a perfect matching (from the name)

English

Let $M$ be a subgraph of $G$. Then $M$ is a perfect matching, if $M$ is a matching and $M$ is a spanning.

Mathlib.Combinatorics.SimpleGraph.Metric

SimpleGraph.balldefMathlib.Combinatorics.SimpleGraph.Metric, function or constant

Wording

the ball of c and r (from the name)

English

Let $G$ be a simple graph of $V$. Let $c$ be an element of $V$. Let $r$ be a natural number. Then the ball of $c$ and $r$ is an element of $\wp V$ defined as $\operatorname{ofPred}$ applied to the function that maps $v$ to the proposition that the extended distance of $v$ and $c$ is less than $r$.

SimpleGraph.distdefMathlib.Combinatorics.SimpleGraph.Metric, function or constant

Wording

the distance of u and v (from the name)

English

Let $G$ be a simple graph of $V$. Let $u$ and $v$ be elements of $V$. Then the distance of $u$ and $v$ is a natural number defined as the natural number of the extended distance of $u$ and $v$.

SimpleGraph.edistdefMathlib.Combinatorics.SimpleGraph.Metric, function or constant

Wording

the extended distance of u and v (from the name)

English

Let $G$ be a simple graph of $V$. Let $u$ and $v$ be elements of $V$. Then the extended distance of $u$ and $v$ is a natural number defined as the infimum of the function that maps $w$ to the length of $w$.

Mathlib.Combinatorics.SimpleGraph.Operations

SimpleGraph.edgedefMathlib.Combinatorics.SimpleGraph.Operations, function or constant

Wording

the edge of s and t (from the name)

English

Let $s$ and $t$ be elements of $V$. Then the edge of $s$ and $t$ is a simple graph of $V$ defined as $\operatorname{fromEdgeSet}$ applied to $\operatorname{singleton}$ applied to $\operatorname{mk}$ applied to $s$ and $t$.

SimpleGraph.replaceVertexdefMathlib.Combinatorics.SimpleGraph.Operations, function or constant

Wording

no wording

English

Let $G$ be a simple graph of $V$. Let $s$ and $t$ be elements of $V$. Then $\operatorname{replaceVertex}$ applied to $G$, $s$ and $t$ is a simple graph of $V$.

Mathlib.Combinatorics.SimpleGraph.Partition

SimpleGraph.Coloring.toPartitiondefMathlib.Combinatorics.SimpleGraph.Partition, function or constant

Wording

the partition of C (from the name)

English

Let $C$ be a coloring of $G$ and $x$. Then the partition of $C$ is a partition of $G$.

SimpleGraph.PartitionstructureMathlib.Combinatorics.SimpleGraph.Partition, type

Wording

partition of G (from the name)

English

Let $G$ be a simple graph of $V$. Then the partitions of $G$ are a basic type.

SimpleGraph.Partition.PartsCardLedefMathlib.Combinatorics.SimpleGraph.Partition, predicate

Wording

no wording

English

Let $P$ be a partition of $G$. Let $n$ be a natural number. Then $\operatorname{PartsCardLe}$ holds for $P$ and $n$, if there exists an element $h$ of $\operatorname{Finite}$ applied to the part of $P$, such that the cardinality of the finite set of $h$ is less than or equal to $n$.

SimpleGraph.Partition.partOfVertexdefMathlib.Combinatorics.SimpleGraph.Partition, function or constant

Wording

the part of P and v (from the name)

English

Let $P$ be a partition of $G$. Let $v$ be an element of $V$. Then the part of $P$ and $v$ is an element of $\wp V$.

SimpleGraph.Partition.partsdefMathlib.Combinatorics.SimpleGraph.Partition, function or constant

Wording

the part of self (from the name)

English

Let $\mathrm{self}$ be a partition of $G$. Then the part of $\mathrm{self}$ is an element of $\wp (\wp V)$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.

SimpleGraph.Partition.toColoringdefMathlib.Combinatorics.SimpleGraph.Partition, function or constant

Wording

the coloring of P (from the name)

English

Let $P$ be a partition of $G$. Then the coloring of $P$ is a coloring of $G$ and the set of elements of the part of $P$.

SimpleGraph.Partition.toColoring'defMathlib.Combinatorics.SimpleGraph.Partition, function or constant

Wording

the coloring of P (from the name)

English

Let $P$ be a partition of $G$. Then the coloring of $P$ is a coloring of $G$ and $\wp V$ defined as $\operatorname{mk}$ applied to $\operatorname{partOfVertex}$ applied to $P$ and the function that maps $x$, $x_{1}$ and $\mathrm{hvw}$ to $\mathrm{SimpleGraph\_\_Partition\_\_partOfVertex\_ne\_of\_adj}$ applied to $P$ and $\mathrm{hvw}$.

SimpleGraph.PartitionabledefMathlib.Combinatorics.SimpleGraph.Partition, predicate

Wording

no wording

English

Let $G$ be a simple graph of $V$. Let $n$ be a natural number. Then $\operatorname{Partitionable}$ holds for $G$ and $n$, if there exists a partition $P$ of $G$, such that $\operatorname{PartsCardLe}$ holds for $P$ and $n$.

Mathlib.Combinatorics.SimpleGraph.Paths

SimpleGraph.PathdefMathlib.Combinatorics.SimpleGraph.Paths, type

Wording

path of u and v (from the name)

English

Let $G$ be a simple graph of $V$. Let $u$ and $v$ be elements of $V$. Then a path of $u$ and $v$ is an element of the function that maps $G$, $u$ and $v$ to $\SubtypeSet {p}{\operatorname{IsPath} (p)}$.

SimpleGraph.Path.mapdefMathlib.Combinatorics.SimpleGraph.Paths, function or constant

Wording

the map of f and p (from the name)

English

Let $f$ be a homomorphism of $G$ and $\mathrm{G'}$ such that $\operatorname{coe}$ applied to $f$ is injective. Let $p$ be a path of $u$ and $v$. Then the map of $f$ and $p$ is a path of $f$ applied to $u$ and $f$ applied to $v$ defined as the map of $f$ and $p$.

SimpleGraph.Path.mapEmbeddingdefMathlib.Combinatorics.SimpleGraph.Paths, function or constant

Wording

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

English

Let $f$ be an embedding of $G$ and $\mathrm{G'}$. Let $p$ be a path of $u$ and $v$. Then the map embedding of $f$ and $p$ is a path of $f$ applied to $u$ and $f$ applied to $v$.

SimpleGraph.Path.nildefMathlib.Combinatorics.SimpleGraph.Paths, function or constant

Wording

no wording

English

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

SimpleGraph.Path.reversedefMathlib.Combinatorics.SimpleGraph.Paths, function or constant

Wording

the reverse of p (from the docstring)

English

Let $p$ be a path of $u$ and $v$. Then the reverse of $p$ is a path of $v$ and $u$ defined as the walk in reverse of $p$.

SimpleGraph.Path.singletondefMathlib.Combinatorics.SimpleGraph.Paths, function or constant

Wording

the singleton of h (from the name)

English

Assume that $\operatorname{Adj}$ holds for $G$, $u$ and $v$. Then the singleton of $h$ is a path of $u$ and $v$ defined as $\operatorname{cons}$ applied to $h$ and $\operatorname{nil}$.

SimpleGraph.Walk.IsCircuitstructureMathlib.Combinatorics.SimpleGraph.Paths, predicate

Wording

p is a circuit (from the name)

English

Let $p$ be a walk of $u$ and $u$. Then we can say that $p$ is a circuit.

SimpleGraph.Walk.IsCyclestructureMathlib.Combinatorics.SimpleGraph.Paths, predicate

Wording

p is a cycle (from the name)

English

Let $p$ be a walk of $u$ and $u$. Then we can say that $p$ is a cycle.

SimpleGraph.Walk.IsPathstructureMathlib.Combinatorics.SimpleGraph.Paths, predicate

Wording

p is a path (from the name)

English

Let $p$ be a walk of $u$ and $v$. Then we can say that $p$ is a path.

SimpleGraph.Walk.IsTrailstructureMathlib.Combinatorics.SimpleGraph.Paths, predicate

Wording

p is a trail (from the name)

English

Let $p$ be a walk of $u$ and $v$. Then we can say that $p$ is a trail.

SimpleGraph.Walk.bypassdefMathlib.Combinatorics.SimpleGraph.Paths, function or constant

Wording

no wording

English

Let $x_{1}$ be a walk of $u$ and $v$. Then $\operatorname{bypass}$ applied to $x_{1}$ is a walk of $u$ and $v$ defined as $\operatorname{brecOn}$ applied to $x_{1}$ and $\mathrm{SimpleGraph\_\_Walk\_\_bypass\_\_\_f}$.

SimpleGraph.Walk.cycleBypassdefMathlib.Combinatorics.SimpleGraph.Paths, function or constant

Wording

no wording

English

Let $x_{1}$ be a walk of $v$ and $v$. Then $\operatorname{cycleBypass}$ applied to $x_{1}$ is a walk of $v$ and $v$.

SimpleGraph.Walk.toPathdefMathlib.Combinatorics.SimpleGraph.Paths, function or constant

Wording

the path of p (from the name)

English

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

Mathlib.Combinatorics.SimpleGraph.Prod

SimpleGraph.Iso.boxProdSumDistribdefMathlib.Combinatorics.SimpleGraph.Prod, function or constant

Wording

no wording

English

Let $G$ be a simple graph of $V$. Let $x_{2}$ be a simple graph of $x$. Let $x_{3}$ be a simple graph of $x_{1}$. Then $\operatorname{boxProdSumDistrib}$ applied to $G$, $x_{2}$ and $x_{3}$ is an isomorphism of $\operatorname{boxProd}$ applied to $G$ and the sum of $x_{2}$ and $x_{3}$ and the sum of $\operatorname{boxProd}$ applied to $G$ and $x_{2}$ and $\operatorname{boxProd}$ applied to $G$ and $x_{3}$.

SimpleGraph.Iso.sumBoxProdDistribdefMathlib.Combinatorics.SimpleGraph.Prod, function or constant

Wording

no wording

English

Let $x_{2}$ be a simple graph of $x$. Let $x_{3}$ be a simple graph of $x_{1}$. Let $H$ be a simple graph of $W$. Then $\operatorname{sumBoxProdDistrib}$ applied to $x_{2}$, $x_{3}$ and $H$ is an isomorphism of $\operatorname{boxProd}$ applied to the sum of $x_{2}$ and $x_{3}$ and $H$ and the sum of $\operatorname{boxProd}$ applied to $x_{2}$ and $H$ and $\operatorname{boxProd}$ applied to $x_{3}$ and $H$.

SimpleGraph.Walk.boxProdLeftdefMathlib.Combinatorics.SimpleGraph.Prod, function or constant

Wording

no wording

English

Let $H$ be a simple graph of $x_{1}$. Let $b$ be an element of $x_{1}$. Let $x_{4}$ be a walk of $x_{2}$ and $x_{3}$. Then $\operatorname{boxProdLeft}$ applied to $H$, $b$ and $x_{4}$ is a walk of $\ProdmkMACRoU {x_{2}}{b}$ and $\ProdmkMACRoU {x_{3}}{b}$ defined as the map of the homomorphism of $\operatorname{boxProdLeft}$ applied to $G$, $H$ and $b$ and $x_{4}$.

SimpleGraph.Walk.boxProdRightdefMathlib.Combinatorics.SimpleGraph.Prod, function or constant

Wording

no wording

English

Let $G$ be a simple graph of $x$. Let $a$ be an element of $x$. Let $x_{4}$ be a walk of $x_{2}$ and $x_{3}$. Then $\operatorname{boxProdRight}$ applied to $G$, $a$ and $x_{4}$ is a walk of $\ProdmkMACRoU {a}{x_{2}}$ and $\ProdmkMACRoU {a}{x_{3}}$ defined as the map of the homomorphism of $\operatorname{boxProdRight}$ applied to $G$, $H$ and $a$ and $x_{4}$.

SimpleGraph.Walk.ofBoxProdLeftdefMathlib.Combinatorics.SimpleGraph.Prod, function or constant

Wording

the walk of x5 (from the name)

English

Let $x_{5}$ be a walk of $x_{4}$ and $y$. Then the walk of $x_{5}$ is a walk of $\ProdfstMACRoZ {x_{4}}$ and $\ProdfstMACRoZ {y}$ defined as $\operatorname{brecOn}$ applied to $x_{5}$ and $\mathrm{SimpleGraph\_\_Walk\_\_ofBoxProdLeft\_\_\_f}$.

SimpleGraph.Walk.ofBoxProdRightdefMathlib.Combinatorics.SimpleGraph.Prod, function or constant

Wording

the walk of x5 (from the name)

English

Let $x_{5}$ be a walk of $x_{4}$ and $y$. Then the walk of $x_{5}$ is a walk of $\ProdsndMACRoAA {x_{4}}$ and $\ProdsndMACRoAA {y}$ defined as $\operatorname{brecOn}$ applied to $x_{5}$ and $\mathrm{SimpleGraph\_\_Walk\_\_ofBoxProdRight\_\_\_f}$.

SimpleGraph.boxProddefMathlib.Combinatorics.SimpleGraph.Prod, function or constant

Wording

no wording

English

Let $G$ be a simple graph of $x$. Let $H$ be a simple graph of $x_{1}$. Then $\operatorname{boxProd}$ applied to $G$ and $H$ is a simple graph of $\mathrm{Prod}$ applied to $x$ and $x_{1}$.

SimpleGraph.boxProdAssocdefMathlib.Combinatorics.SimpleGraph.Prod, function or constant

Wording

no wording

English

Let $G$ be a simple graph of $x$. Let $H$ be a simple graph of $x_{1}$. Let $I$ be a simple graph of $x_{2}$. Then $\operatorname{boxProdAssoc}$ applied to $G$, $H$ and $I$ is an isomorphism of $\operatorname{boxProd}$ applied to $\operatorname{boxProd}$ applied to $G$ and $H$ and $I$ and $\operatorname{boxProd}$ applied to $G$ and $\operatorname{boxProd}$ applied to $H$ and $I$.

SimpleGraph.boxProdCommdefMathlib.Combinatorics.SimpleGraph.Prod, function or constant

Wording

no wording

English

Let $G$ be a simple graph of $x$. Let $H$ be a simple graph of $x_{1}$. Then $\operatorname{boxProdComm}$ applied to $G$ and $H$ is an isomorphism of $\operatorname{boxProd}$ applied to $G$ and $H$ and $\operatorname{boxProd}$ applied to $H$ and $G$.

SimpleGraph.boxProdLeftdefMathlib.Combinatorics.SimpleGraph.Prod, function or constant

Wording

no wording

English

Let $G$ be a simple graph of $x$. Let $H$ be a simple graph of $x_{1}$. Let $b$ be an element of $x_{1}$. Then $\operatorname{boxProdLeft}$ applied to $G$, $H$ and $b$ is an embedding of $G$ and $\operatorname{boxProd}$ applied to $G$ and $H$.

SimpleGraph.boxProdRightdefMathlib.Combinatorics.SimpleGraph.Prod, function or constant

Wording

no wording

English

Let $G$ be a simple graph of $x$. Let $H$ be a simple graph of $x_{1}$. Let $a$ be an element of $x$. Then $\operatorname{boxProdRight}$ applied to $G$, $H$ and $a$ is an embedding of $H$ and $\operatorname{boxProd}$ applied to $G$ and $H$.

Mathlib.Combinatorics.SimpleGraph.Regularity.Bound

SzemerediRegularity.Positivity.tacticSz_positivitydefMathlib.Combinatorics.SimpleGraph.Regularity.Bound, function or constant

Wording

no wording

English

generation took over the time limit

SzemerediRegularity.bounddefMathlib.Combinatorics.SimpleGraph.Regularity.Bound, function or constant

Wording

the bound of x and l (from the name)

English

Let $x$ be a real number. Let $l$ be a natural number. Then the bound of $x$ and $l$ is a natural number defined as the product of $\operatorname{iterate}$ applied to $\operatorname{stepBound}$, the floor of $\frac{ 4}{x ^ {5}}$ and $\operatorname{initialBound}$ applied to $x$ and $l$ and the exponentiation of $16$ to $\operatorname{iterate}$ applied to $\operatorname{stepBound}$, the floor of $\frac{ 4}{x ^ {5}}$ and $\operatorname{initialBound}$ applied to $x$ and $l$.

Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk

SzemerediRegularity.chunkdefMathlib.Combinatorics.SimpleGraph.Regularity.Chunk, function or constant

Wording

no wording

English

Assume that $P$ is an equipartition. Let $G$ be a simple graph of $x$. Let $x_{4}$ be a real number. Assume that $U$ is an element of the set of parts of $P$. Then $\operatorname{chunk}$ applied to $\mathrm{hP}$, $G$, $x_{4}$ and $\mathrm{hU}$ is a finpartition of $U$ defined as $\mathrm{dite}$ applied to the proposition that the cardinality of $U$ is equal to the sum of the product of the quotient of the cardinality of $x$ and $\operatorname{stepBound}$ applied to the cardinality of the set of parts of $P$ and the exponentiation of $4$ to the cardinality of the set of parts of $P$ and the difference between the quotient of the cardinality of $x$ and the cardinality of the set of parts of $P$ and the product of the quotient of the cardinality of $x$ and $\operatorname{stepBound}$ applied to the cardinality of the set of parts of $P$ and the exponentiation of $4$ to the cardinality of the set of parts of $P$, the function that maps $\mathrm{hUcard}$ to $\operatorname{equitabilise}$ applied to $\mathrm{SzemerediRegularity\_\_card\_aux\_u2081\_}$ applied to $\mathrm{hUcard}$ and the function that maps $\mathrm{hUcard1}$ to $\operatorname{equitabilise}$ applied to $\mathrm{SzemerediRegularity\_\_card\_aux\_u2082\_}$ applied to $\mathrm{hP}$, $\mathrm{hU}$ and $\mathrm{hUcard1}$.

SzemerediRegularity.stardefMathlib.Combinatorics.SimpleGraph.Regularity.Chunk, function or constant

Wording

the star of x4 and V (from the name)

English

Assume that $P$ is an equipartition. Let $G$ be a simple graph of $x$. Let $x_{4}$ be an element of $\Real$. Assume that $\MembershipmemMACRoT {\operatorname{parts} (P)}{U}$. Let $V$ be a finite set of $x$. Then the star of $x_{4}$ and $V$ is a finite set of the set of finite sets of $x$ defined as $\FinsetFilter {A}{\mathrm{Leq} (A , \operatorname{nonuniformWitness} (G , x_{4} , U , V))}{\operatorname{parts} (\operatorname{chunk} (\mathrm{hP} , G , x_{4} , \mathrm{hU}))}$.

Mathlib.Combinatorics.SimpleGraph.Regularity.Energy

Finpartition.energydefMathlib.Combinatorics.SimpleGraph.Regularity.Energy, function or constant

Wording

the energy of P and G (from the docstring)

English

Let $P$ be a finpartition of $s$. Let $G$ be a simple graph of $x$. Then the energy of $P$ and $G$ is an element of $\Rational$ defined as $\frac{ \FinsetSum {\operatorname{offDiag} (\operatorname{parts} (P))}{\mathrm{uv}}{(\operatorname{edgeDensity} (\ProdfstMACRoZ {\mathrm{uv}}, \ProdsndMACRoAA {\mathrm{uv}})^ {2})}}{\FinsetcardMACRoM {\operatorname{parts} (P)}^ {2}}$.