birkhoffAveragedefMathlib.Dynamics.BirkhoffSum.Average, function or constantEnglish
Let $R$ be a set. Let $f$ be a function from elements of $x$ to elements of $x$. Let $g$ be a function from elements of $x$ to elements of $M$. Let $n$ be a natural number. Let $x_{4}$ be an element of $x$. Then $\mathrm{birkhoffAverage}$ applied to $R$, $f$, $g$, $n$ and $x_{4}$ is an element of $M$ defined as $\HSMulhSMulMACRoAL {\operatorname{inv} (n)}{\mathrm{birkhoffSum} (f , g , n , x_{4})}$.
birkhoffSumdefMathlib.Dynamics.BirkhoffSum.Basic, function or constantEnglish
Let $f$ be a function from elements of $x$ to elements of $x$. Let $g$ be a function from elements of $x$ to elements of $M$. Let $n$ be a natural number. Let $x_{2}$ be an element of $x$. Then $\mathrm{birkhoffSum}$ applied to $f$, $g$, $n$ and $x_{2}$ is an element of $M$ defined as $\FinsetSum {\FinsetrangeMACRoN {n}}{k}{g (\operatorname{iterate} (f , k , x_{2}))}$.
CircleDeg1LiftstructureMathlib.Dynamics.Circle.RotationNumber.TranslationNumber, typeWording
circle degree lift (from the name)
English
The circle degree lifts are a basic type.
CircleDeg1Lift.toOrderIsodefMathlib.Dynamics.Circle.RotationNumber.TranslationNumber, function or constantWording
the order isomorphism (from the name)
English
The order isomorphism is a monoid homomorphism of the set of units of the set of circle degree lifts and the set of order isomorphisms of $\Real$ and $\Real$.
CircleDeg1Lift.translatedefMathlib.Dynamics.Circle.RotationNumber.TranslationNumber, function or constantEnglish
$\operatorname{translate}$ is a monoid homomorphism of the set of multiplicatives of $\Real$ and the set of units of the set of circle degree lifts.
CircleDeg1Lift.translationNumberdefMathlib.Dynamics.Circle.RotationNumber.TranslationNumber, function or constantWording
the translation number of f (from the docstring)
English
Let $f$ be a circle degree lift. Then the translation number of $f$ is a real number defined as $\operatorname{limUnder}$ applied to $\operatorname{atTop}$ and $\operatorname{transnumAuxSeq}$ applied to $f$.
ErgodicSMulclassMathlib.Dynamics.Ergodic.Action.Basic, predicateWording
x3 is a ergodic product (from the name)
English
Let $G$ and $x$ be sets. Let $x_{3}$ be a measure of $x$. Then we can say that $x_{3}$ is an ergodic product.
ErgodicVAddclassMathlib.Dynamics.Ergodic.Action.Basic, predicateWording
x3 is a ergodic sum (from the name)
English
Let $G$ and $x$ be sets. Let $x_{3}$ be a measure of $x$. Then we can say that $x_{3}$ is an ergodic sum.
MeasureTheory.ConservativestructureMathlib.Dynamics.Ergodic.Conservative, predicateWording
f is conservative with respect to x2 (from the name)
English
Let $f$ be a function from elements of $x$ to elements of $x$. Let $x_{2}$ be a measure of $x$. Then we can say that $f$ is conservative with respect to $x_{2}$.
MeasureTheory.empiricalMeasuredefMathlib.Dynamics.Ergodic.EmpiricalMeasure, function or constantWording
the empirical measure of x1 and n (from the name)
English
Let $f$ be a function from elements of $X$ to elements of $X$. Let $x_{1}$ be an element of $X$. Let $n$ be a natural number. Then the empirical measure of $x_{1}$ and $n$ is a measure of $X$ defined as $\mathrm{birkhoffAverage}$ applied to $\mathrm{NNReal}$, $f$, $\operatorname{dirac}$, $n + 1$ and $x_{1}$.
ErgodicstructureMathlib.Dynamics.Ergodic.Ergodic, predicateWording
f is ergodic to x1 (from the name)
English
Let $f$ be a function from elements of $x$ to elements of $x$. Let $x_{1}$ be an element of $\mathrm{autoParam}$ applied to the set of measures of $x$ and $\mathrm{Ergodic\_\_\_auto\_1}$. Then we can say that $f$ is ergodic to $x_{1}$.
PreErgodicstructureMathlib.Dynamics.Ergodic.Ergodic, predicateWording
f is ergodic to x1 (from the name)
English
Let $f$ be a function from elements of $x$ to elements of $x$. Let $x_{1}$ be an element of $\mathrm{autoParam}$ applied to the set of measures of $x$ and $\mathrm{PreErgodic\_\_\_auto\_1}$. Then we can say that $f$ is ergodic to $x_{1}$.
QuasiErgodicstructureMathlib.Dynamics.Ergodic.Ergodic, predicateEnglish
Let $f$ be a function from elements of $x$ to elements of $x$. Let $x_{1}$ be an element of $\mathrm{autoParam}$ applied to the set of measures of $x$ and $\mathrm{QuasiErgodic\_\_\_auto\_1}$. Then we can say that $\mathrm{QuasiErgodic}$ holds for $f$ and $x_{1}$.
MeasureTheory.MeasurePreservingstructureMathlib.Dynamics.Ergodic.MeasurePreserving, predicateEnglish
Let $f$ be a function from elements of $x$ to elements of $x_{1}$. Let $x_{4}$ be an element of $\mathrm{autoParam}$ applied to the set of measures of $x$ and $\mathrm{MeasureTheory\_\_MeasurePreserving\_\_\_auto\_1}$. Let $x_{5}$ be an element of $\mathrm{autoParam}$ applied to the set of measures of $x_{1}$ and $\mathrm{MeasureTheory\_\_MeasurePreserving\_\_\_auto\_3}$. Then we can say that $\operatorname{MeasurePreserving}$ holds for $f$, $x_{4}$ and $x_{5}$.
Function.fixedPointsdefMathlib.Dynamics.FixedPoints.Defs, function or constantWording
the fixed point of f (from the name)
English
Let $f$ be a function from elements of $x$ to elements of $x$. Then the fixed point of $f$ is an element of $\wp x$ defined as $\operatorname{ofPred}$ applied to the function that maps $x_{1}$ to $\operatorname{IsFixedPt}$ applied to $f$ and $x_{1}$.
Function.HasCompactFixedSupportdefMathlib.Dynamics.FixedPoints.Support, predicateWording
f has compact fixed supports (from the name)
English
Let $f$ be a function from elements of $X$ to elements of $X$. Then $f$ has compact fixed supports, if the fixed support of $f$ is compact.
Function.fixedSupportdefMathlib.Dynamics.FixedPoints.Support, function or constantWording
the fixed support of f (from the docstring)
English
Let $f$ be a function from elements of $X$ to elements of $X$. Then the fixed support of $f$ is an element of $\wp X$ defined as the closure of the complement of the fixed point of $f$.
FlowstructureMathlib.Dynamics.Flow, typeWording
flow of x and x1 (from the name)
English
Let $x$ and $x_{1}$ be sets. Then the flows of $x$ and $x_{1}$ are a basic type.
Flow.IsFactorOfdefMathlib.Dynamics.Flow, predicateEnglish
Let $x_{7}$ be a flow of $x$ and $x_{5}$. Let $x_{8}$ be a flow of $x$ and $x_{1}$. Then $\operatorname{IsFactorOf}$ holds for $x_{7}$ and $x_{8}$, if there exists a function $x_{9}$ from elements of $x_{1}$ to elements of $x_{5}$, such that $\operatorname{IsSemiconjugacy}$ holds for $x_{9}$, $x_{8}$ and $x_{7}$.
Flow.IsSemiconjugacystructureMathlib.Dynamics.Flow, predicateEnglish
Let $x_{7}$ be a function from elements of $x_{1}$ to elements of $x_{5}$. Let $x_{8}$ be a flow of $x$ and $x_{1}$. Let $x_{9}$ be a flow of $x$ and $x_{5}$. Then we can say that $\operatorname{IsSemiconjugacy}$ holds for $x_{7}$, $x_{8}$ and $x_{9}$.
Flow.forwardOrbitdefMathlib.Dynamics.Flow, function or constantWording
the forward orbit of x5 and x7 (from the docstring)
English
Let $x_{5}$ be a flow of $x$ and $x_{1}$. Let $x_{7}$ be an element of $x_{1}$. Then the forward orbit of $x_{5}$ and $x_{7}$ is an element of $\wp x_{1}$ defined as the orbit of $\operatorname{restrictNonneg}$ applied to $x_{5}$ and $x_{7}$.
Flow.fromIterdefMathlib.Dynamics.Flow, function or constantEnglish
Assume that $g$ is continuous. Then $\operatorname{fromIter}$ applied to $h$ is a flow of $\Natural$ and $x$.
Flow.iddefMathlib.Dynamics.Flow, function or constantWording
the identity map of x and x1 (from the docstring)
English
Let $x$ and $x_{1}$ be sets. Then the identity map of $x$ and $x_{1}$ is a flow of $x$ and $x_{1}$.
Flow.orbitdefMathlib.Dynamics.Flow, function or constantWording
the orbit of x5 and x6 (from the docstring)
English
Let $x_{5}$ be a flow of $x$ and $x_{1}$. Let $x_{6}$ be an element of $x_{1}$. Then the orbit of $x_{5}$ and $x_{6}$ is an element of $\wp x_{1}$ defined as the orbit of $x$ and $x_{6}$.
Flow.restrictdefMathlib.Dynamics.Flow, function or constantEnglish
Let $x_{5}$ be a flow of $x$ and $x_{1}$. Assume that $\mathrm{IsInvariant}$ holds for $\operatorname{toFun}$ and $s$. Then $\operatorname{restrict}$ applied to $x_{5}$ and $h$ is a flow of $x$ and the set of elements of $s$.
Flow.restrictAddSubmonoiddefMathlib.Dynamics.Flow, function or constantEnglish
Let $x_{5}$ be a flow of $x$ and $x_{1}$. Let $S$ be an additive submonoid of $x$. Then $\operatorname{restrictAddSubmonoid}$ applied to $x_{5}$ and $S$ is a flow of $\SubtypeSet {x_{6}}{(\MembershipmemMACRoT {S}{x_{6}})}$ and $x_{1}$.
Flow.restrictNonnegdefMathlib.Dynamics.Flow, function or constantEnglish
Let $x_{5}$ be a flow of $x$ and $x_{1}$. Then $\operatorname{restrictNonneg}$ applied to $x_{5}$ is a flow of $\SubtypeSet {x_{7}}{(\MembershipmemMACRoT {\operatorname{nonneg} (x)}{x_{7}})}$ and $x_{1}$ defined as $\operatorname{restrictAddSubmonoid}$ applied to $x_{5}$ and $\operatorname{nonneg}$ applied to $x$.
Flow.reversedefMathlib.Dynamics.Flow, function or constantWording
the reverse of x5 (from the name)
English
Let $x_{5}$ be a flow of $x$ and $x_{1}$. Then the reverse of $x_{5}$ is a flow of $x$ and $x_{1}$.
Flow.toFundefMathlib.Dynamics.Flow, function or constantWording
the flow of x5 and x6 (from the name)
English
Let $\mathrm{self}$ be a flow of $x$ and $x_{1}$. Let $x_{5}$ be an element of $x$. Let $x_{6}$ be an element of $x_{1}$. Then the flow of $x_{5}$ and $x_{6}$ is an element of $x_{1}$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$, $x_{5}$ and $x_{6}$.
Flow.toHomeomorphdefMathlib.Dynamics.Flow, function or constantWording
the homeomorphism of x5 and t (from the name)
English
Let $x_{5}$ be a flow of $x$ and $x_{1}$. Let $t$ be an element of $x$. Then the homeomorphism of $x_{5}$ and $t$ is a homeomorphism of $x_{1}$ and $x_{1}$.
Homeomorph.flowdefMathlib.Dynamics.Flow, function or constantWording
the discrete flow of f (from the docstring)
English
Let $f$ be a homeomorphism of $x$ and $x$. Then the discrete flow of $f$ is a flow of $\Integer$ and $x$.
IsForwardInvariantdefMathlib.Dynamics.Flow, predicateEnglish
Let $x_{4}$ be a function from elements of $x$ and elements of $x_{1}$ to elements of $x_{1}$. Let $s$ be an element of $\wp x_{1}$. Then $\mathrm{IsForwardInvariant}$ holds for $x_{4}$ and $s$, if for all elements $t$ of $x$, if $0 \leq t$, then $\operatorname{MapsTo}$ holds for $x_{4}$ applied to $t$, $s$ and $s$.
IsInvariantdefMathlib.Dynamics.Flow, predicateEnglish
Let $x_{2}$ be a function from elements of $x$ and elements of $x_{1}$ to elements of $x_{1}$. Let $s$ be an element of $\wp x_{1}$. Then $\mathrm{IsInvariant}$ holds for $x_{2}$ and $s$, if for all elements $t$ of $x$, $\operatorname{MapsTo}$ holds for $x_{2}$ applied to $t$, $s$ and $s$.
AddAction.IsMinimalclassMathlib.Dynamics.Minimal, predicateEnglish
Let $M$ and $x$ be sets. Then we can say that $\operatorname{IsMinimal}$ holds for $M$ and $x$.
MulAction.IsMinimalclassMathlib.Dynamics.Minimal, predicateEnglish
Let $M$ and $x$ be sets. Then we can say that $\operatorname{IsMinimal}$ holds for $M$ and $x$.
Polynomial.newtonMapdefMathlib.Dynamics.Newton, function or constantEnglish
Let $P$ be a polynomial of $R$. Let $x_{3}$ be an element of $S$. Then $\operatorname{newtonMap}$ applied to $P$ and $x_{3}$ is an element of $S$ defined as the difference between $x_{3}$ and the product of the inverse of $\operatorname{aeval}$ applied to $x_{3}$ and $\operatorname{derivative}$ applied to $P$ and $\operatorname{aeval}$ applied to $x_{3}$ and $P$.
omegaLimitdefMathlib.Dynamics.OmegaLimit, function or constantWording
the omega limit of x4 and s (from the name)
English
Let $f$ be a filter of $x$. Let $x_{4}$ be a function from elements of $x$ and elements of $x_{1}$ to elements of $x_{2}$. Let $s$ be an element of $\wp x_{1}$. Then the omega limit of $x_{4}$ and $s$ is an element of $\wp x_{2}$ defined as the intersection of the function that maps $u$ to the intersection of the function that maps $h$ to the closure of the image of $u$ and $s$.
AddAction.perioddefMathlib.Dynamics.PeriodicPts.Defs, function or constantWording
the period of m and a (from the docstring)
English
Let $m$ be an element of $M$. Let $a$ be an element of $x$. Then the period of $m$ and $a$ is a natural number defined as the minimal period of the function that maps $x_{3}$ to the sum of $m$ and $x_{3}$ and $a$.
Function.IsPeriodicPtdefMathlib.Dynamics.PeriodicPts.Defs, predicateEnglish
Let $f$ be a function from elements of $x$ to elements of $x$. Let $n$ be a natural number. Let $x_{1}$ be an element of $x$. Then $\operatorname{IsPeriodicPt}$ holds for $f$, $n$ and $x_{1}$, if $\operatorname{IsFixedPt}$ holds for $\operatorname{iterate}$ applied to $f$ and $n$ and $x_{1}$.
Function.minimalPerioddefMathlib.Dynamics.PeriodicPts.Defs, function or constantWording
the minimal period of f and x1 (from the name)
English
Let $f$ be a function from elements of $x$ to elements of $x$. Let $x_{1}$ be an element of $x$. Then the minimal period of $f$ and $x_{1}$ is a natural number defined as $\mathrm{dite}$ applied to $\MembershipmemMACRoT {\operatorname{periodicPts} (f)}{x_{1}}$, the function that maps $h$ to $\operatorname{find}$ applied to $h$ and the function that maps $h_{1}$ to $0$.
Function.periodicOrbitdefMathlib.Dynamics.PeriodicPts.Defs, function or constantWording
the orbit of f and x1 (from the docstring)
English
Let $f$ be a function from elements of $x$ to elements of $x$. Let $x_{1}$ be an element of $x$. Then the orbit of $f$ and $x_{1}$ is a cycle of $x$ defined as the cycle of $\operatorname{map}$ applied to the function that maps $n$ to $\operatorname{iterate}$ applied to $f$, $n$ and $x_{1}$ and $\operatorname{range}$ applied to the minimal period of $f$ and $x_{1}$.
Function.periodicPtsdefMathlib.Dynamics.PeriodicPts.Defs, function or constantEnglish
Let $f$ be a function from elements of $x$ to elements of $x$. Then $\operatorname{periodicPts}$ applied to $f$ is an element of $\wp x$ defined as $\operatorname{ofPred}$ applied to the function that maps $x_{1}$ to the proposition that there exists a natural number $n$, such that $n > 0$ and $\operatorname{IsPeriodicPt}$ holds for $f$, $n$ and $x_{1}$.
Function.ptsOfPerioddefMathlib.Dynamics.PeriodicPts.Defs, function or constantEnglish
Let $f$ be a function from elements of $x$ to elements of $x$. Let $n$ be a natural number. Then $\operatorname{ptsOfPeriod}$ applied to $f$ and $n$ is an element of $\wp x$ defined as $\operatorname{ofPred}$ applied to the function that maps $x_{1}$ to $\operatorname{IsPeriodicPt}$ applied to $f$, $n$ and $x_{1}$.
MulAction.perioddefMathlib.Dynamics.PeriodicPts.Defs, function or constantWording
the period of m and a (from the docstring)
English
Let $m$ be an element of $M$. Let $a$ be an element of $x$. Then the period of $m$ and $a$ is a natural number defined as the minimal period of the function that maps $x_{3}$ to $\HSMulhSMulMACRoAL {m}{x_{3}}$ and $a$.
SymbolicDynamics.FullShift.LanguageOndefMathlib.Dynamics.SymbolicDynamics.Basic, function or constantWording
the language of X and U (from the docstring)
English
Let $X$ be an element of $\wp (\mathrm{Elem} (G)\rightarrow A)$. Let $U$ be a finite set of $G$. Then the language of $X$ and $U$ is an element of the power set of the set of patterns of $A$ and $G$ defined as $\operatorname{ofPred}$ applied to the function that maps $p$ to the proposition that there exists a function $x_{1}$ from elements of $G$ to elements of $A$, such that $x_{1}$ is an element of $X$ and $\EqtMACRoH {\operatorname{fromConfig} (x_{1} , U)}{p}$.
SymbolicDynamics.FullShift.MulSubshiftstructureMathlib.Dynamics.SymbolicDynamics.Basic, typeWording
multiplicative subshift of A and G (from the name)
English
Let $A$ and $G$ be sets. Then the multiplicative subshifts of $A$ and $G$ are a basic type.
SymbolicDynamics.FullShift.MulSubshift.carrierdefMathlib.Dynamics.SymbolicDynamics.Basic, function or constantWording
the carrier of self (from the name)
English
Let $\mathrm{self}$ be a multiplicative subshift of $A$ and $G$. Then the carrier of $\mathrm{self}$ is an element of $\wp (\mathrm{Elem} (G)\rightarrow A)$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.
SymbolicDynamics.FullShift.MulSubshift.languageOndefMathlib.Dynamics.SymbolicDynamics.Basic, function or constantWording
the language of Y and U (from the docstring)
English
Let $Y$ be a multiplicative subshift of $A$ and $G$. Let $U$ be a finite set of $G$. Then the language of $Y$ and $U$ is an element of the power set of the set of patterns of $A$ and $G$ defined as the language of the carrier of $Y$ and $U$.
SymbolicDynamics.FullShift.MulSubshift.ofForbiddendefMathlib.Dynamics.SymbolicDynamics.Basic, function or constantWording
the multiplicative subshift of F (from the name)
English
Let $F$ be an element of the power set of the set of patterns of $A$ and $G$. Then the multiplicative subshift of $F$ is a multiplicative subshift of $A$ and $G$ defined as $\operatorname{mk}$ applied to $\operatorname{mulForbidden}$ applied to $F$, $\mathrm{SymbolicDynamics\_\_FullShift\_\_isClosed\_mulForbidden}$ applied to $F$ and $\mathrm{SymbolicDynamics\_\_FullShift\_\_Pattern\_\_mapsTo\_mulShift\_mulForbidden}$ applied to $F$.
SymbolicDynamics.FullShift.PatternstructureMathlib.Dynamics.SymbolicDynamics.Basic, typeWording
pattern of A and G (from the name)
English
Let $A$ and $G$ be sets. Then the patterns of $A$ and $G$ are a basic type.
SymbolicDynamics.FullShift.Pattern.configdefMathlib.Dynamics.SymbolicDynamics.Basic, function or constantWording
the full configuration in the full shift of self and x1 (from the docstring)
English
Let $\mathrm{self}$ be a pattern of $A$ and $G$. Let $x_{1}$ be an element of $G$. Then the full configuration in the full shift of $\mathrm{self}$ and $x_{1}$ is an element of $A$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$ and $x_{1}$.
SymbolicDynamics.FullShift.Pattern.fromConfigdefMathlib.Dynamics.SymbolicDynamics.Basic, function or constantEnglish
Let $x_{1}$ be a function from elements of $G$ to elements of $A$. Let $U$ be a finite set of $G$. Then $\operatorname{fromConfig}$ applied to $x_{1}$ and $U$ is a pattern of $A$ and $G$.
SymbolicDynamics.FullShift.Pattern.mulOccursInAtdefMathlib.Dynamics.SymbolicDynamics.Basic, predicateEnglish
Let $p$ be a pattern of $A$ and $G$. Let $x_{2}$ be a function from elements of $G$ to elements of $A$. Let $g$ be an element of $G$. Then $\operatorname{mulOccursInAt}$ holds for $p$, $x_{2}$ and $g$, if for all elements $h$ of $G$, if $h$ is an element of the support of $p$, then $x_{2}$ applied to $g \times h$ is equal to the full configuration in the full shift of $p$ and $h$.
SymbolicDynamics.FullShift.Pattern.mulShiftdefMathlib.Dynamics.SymbolicDynamics.Basic, function or constantWording
the multiplicative shift of v and x2 (from the name)
English
Let $p$ be a pattern of $A$ and $G$. Let $v$ and $x_{2}$ be elements of $G$. Then the multiplicative shift of $v$ and $x_{2}$ is an element of $A$.
SymbolicDynamics.FullShift.Pattern.occursInAtdefMathlib.Dynamics.SymbolicDynamics.Basic, predicateEnglish
Let $p$ be a pattern of $A$ and $G$. Let $x_{2}$ be a function from elements of $G$ to elements of $A$. Let $g$ be an element of $G$. Then $\operatorname{occursInAt}$ holds for $p$, $x_{2}$ and $g$, if for all elements $h$ of $G$, if $h$ is an element of the support of $p$, then $x_{2}$ applied to $g + h$ is equal to the full configuration in the full shift of $p$ and $h$.
SymbolicDynamics.FullShift.Pattern.shiftdefMathlib.Dynamics.SymbolicDynamics.Basic, function or constantWording
the shift of v and x2 (from the name)
English
Let $p$ be a pattern of $A$ and $G$. Let $v$ and $x_{2}$ be elements of $G$. Then the shift of $v$ and $x_{2}$ is an element of $A$.
SymbolicDynamics.FullShift.Pattern.supportdefMathlib.Dynamics.SymbolicDynamics.Basic, function or constantWording
the support of self (from the name)
English
Let $\mathrm{self}$ be a pattern of $A$ and $G$. Then the support of $\mathrm{self}$ is a finite set of $G$ defined as $\operatorname{proj1}$ applied to $\mathrm{self}$.
SymbolicDynamics.FullShift.SubshiftstructureMathlib.Dynamics.SymbolicDynamics.Basic, typeWording
subshift of A and G (from the name)
English
Let $A$ and $G$ be sets. Then the subshifts of $A$ and $G$ are a basic type.
SymbolicDynamics.FullShift.Subshift.carrierdefMathlib.Dynamics.SymbolicDynamics.Basic, function or constantWording
the carrier of self (from the name)
English
Let $\mathrm{self}$ be a subshift of $A$ and $G$. Then the carrier of $\mathrm{self}$ is an element of $\wp (\mathrm{Elem} (G)\rightarrow A)$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.
SymbolicDynamics.FullShift.Subshift.ofForbiddendefMathlib.Dynamics.SymbolicDynamics.Basic, function or constantWording
the subshift of F (from the name)
English
Let $F$ be an element of the power set of the set of patterns of $A$ and $G$. Then the subshift of $F$ is a subshift of $A$ and $G$ defined as $\operatorname{mk}$ applied to $\operatorname{forbidden}$ applied to $F$, $\mathrm{SymbolicDynamics\_\_FullShift\_\_isClosed\_forbidden}$ applied to $F$ and $\mathrm{SymbolicDynamics\_\_FullShift\_\_Pattern\_\_mapsTo\_shift\_forbidden}$ applied to $F$.
SymbolicDynamics.FullShift.cylinderdefMathlib.Dynamics.SymbolicDynamics.Basic, function or constantWording
the cylinder of U and x (from the name)
English
Let $U$ be a finite set of $G$. Let $x$ be a function from elements of $G$ to elements of $A$. Then the cylinder of $U$ and $x$ is an element of $\wp (\mathrm{Elem} (G)\rightarrow A)$ defined as $\operatorname{ofPred}$ applied to the function that maps $y$ to the proposition that for all elements $i$ of $G$, if $i$ is an element of $U$, then $\EqtMACRoH {y (i)}{x (i)}$.
SymbolicDynamics.FullShift.forbiddendefMathlib.Dynamics.SymbolicDynamics.Basic, function or constantEnglish
Let $F$ be an element of the power set of the set of patterns of $A$ and $G$. Then $\operatorname{forbidden}$ applied to $F$ is an element of $\wp (\mathrm{Elem} (G)\rightarrow A)$ defined as $\operatorname{ofPred}$ applied to the function that maps $x_{2}$ to the proposition that for all patterns $p$ of $A$ and $G$, if $p$ is an element of $F$, then for all elements $g$ of $G$, it is not the case that $\operatorname{occursInAt}$ holds for $p$, $x_{2}$ and $g$.
SymbolicDynamics.FullShift.fullShiftdefMathlib.Dynamics.SymbolicDynamics.Basic, function or constantWording
the full shift of A and G (from the name)
English
Let $A$ and $G$ be sets. Then the full shift of $A$ and $G$ is a subshift of $A$ and $G$.
SymbolicDynamics.FullShift.mulForbiddendefMathlib.Dynamics.SymbolicDynamics.Basic, function or constantEnglish
Let $F$ be an element of the power set of the set of patterns of $A$ and $G$. Then $\operatorname{mulForbidden}$ applied to $F$ is an element of $\wp (\mathrm{Elem} (G)\rightarrow A)$ defined as $\operatorname{ofPred}$ applied to the function that maps $x_{2}$ to the proposition that for all patterns $p$ of $A$ and $G$, if $p$ is an element of $F$, then for all elements $g$ of $G$, it is not the case that $\operatorname{mulOccursInAt}$ holds for $p$, $x_{2}$ and $g$.
SymbolicDynamics.FullShift.mulFullShiftdefMathlib.Dynamics.SymbolicDynamics.Basic, function or constantWording
the multiplicative full shift of A and G (from the name)
English
Let $A$ and $G$ be sets. Then the multiplicative full shift of $A$ and $G$ is a multiplicative subshift of $A$ and $G$.
SymbolicDynamics.FullShift.mulShiftdefMathlib.Dynamics.SymbolicDynamics.Basic, function or constantWording
the multiplicative shift of x1 and x2 (from the name)
English
Let $g$ and $x_{2}$ be elements of $G$. Let $x_{1}$ be a function from elements of $G$ to elements of $A$. Then the multiplicative shift of $x_{1}$ and $x_{2}$ is an element of $A$ defined as $x_{1}$ applied to $g \times x_{2}$.
SymbolicDynamics.FullShift.shiftdefMathlib.Dynamics.SymbolicDynamics.Basic, function or constantWording
the shift of x1 and x2 (from the name)
English
Let $g$ and $x_{2}$ be elements of $G$. Let $x_{1}$ be a function from elements of $G$ to elements of $A$. Then the shift of $x_{1}$ and $x_{2}$ is an element of $A$ defined as $x_{1}$ applied to $g + x_{2}$.
Dynamics.IsDynCoverOfdefMathlib.Dynamics.TopologicalEntropy.CoverEntropy, predicateEnglish
Let $T$ be a function from elements of $X$ to elements of $X$. Let $F$ and $s$ be elements of $\wp X$. Let $U$ be a set relation of $X$ and $X$. Let $n$ be a natural number. Then $\operatorname{IsDynCoverOf}$ holds for $T$, $F$, $U$, $n$ and $s$, if $\operatorname{IsCover}$ holds for $\operatorname{dynEntourage}$ applied to $T$, $U$ and $n$, $F$ and $s$.
Dynamics.coverEntropydefMathlib.Dynamics.TopologicalEntropy.CoverEntropy, function or constantWording
the cover entropy of T and F (from the name)
English
Let $T$ be a function from elements of $X$ to elements of $X$. Let $F$ be an element of $\wp X$. Then the cover entropy of $T$ and $F$ is an element of $\mathrm{EReal}$ defined as the supremum of the function that maps $U$ to the supremum of the function that maps $h$ to the cover entropy entourage of $F$ and $U$.
Dynamics.coverEntropyEntouragedefMathlib.Dynamics.TopologicalEntropy.CoverEntropy, function or constantWording
the cover entropy entourage of F and U (from the name)
English
Let $T$ be a function from elements of $X$ to elements of $X$. Let $F$ be an element of $\wp X$. Let $U$ be a set relation of $X$ and $X$. Then the cover entropy entourage of $F$ and $U$ is an element of $\mathrm{EReal}$ defined as the exponential growth supremum of the function that maps $n$ to $\operatorname{toENNReal}$ applied to $\operatorname{coverMincard}$ applied to $T$, $F$, $U$ and $n$.
Dynamics.coverEntropyInfdefMathlib.Dynamics.TopologicalEntropy.CoverEntropy, function or constantWording
the cover entropy infimum of T and F (from the name)
English
Let $T$ be a function from elements of $X$ to elements of $X$. Let $F$ be an element of $\wp X$. Then the cover entropy infimum of $T$ and $F$ is an element of $\mathrm{EReal}$ defined as the supremum of the function that maps $U$ to the supremum of the function that maps $h$ to the cover entropy infimum entourage of $F$ and $U$.
Dynamics.coverEntropyInfEntouragedefMathlib.Dynamics.TopologicalEntropy.CoverEntropy, function or constantWording
the cover entropy infimum entourage of F and U (from the name)
English
Let $T$ be a function from elements of $X$ to elements of $X$. Let $F$ be an element of $\wp X$. Let $U$ be a set relation of $X$ and $X$. Then the cover entropy infimum entourage of $F$ and $U$ is an element of $\mathrm{EReal}$ defined as the exponential growth infimum of the function that maps $n$ to $\operatorname{toENNReal}$ applied to $\operatorname{coverMincard}$ applied to $T$, $F$, $U$ and $n$.
Dynamics.coverMincarddefMathlib.Dynamics.TopologicalEntropy.CoverEntropy, function or constantEnglish
Let $T$ be a function from elements of $X$ to elements of $X$. Let $F$ be an element of $\wp X$. Let $U$ be a set relation of $X$ and $X$. Let $n$ be a natural number. Then $\operatorname{coverMincard}$ applied to $T$, $F$, $U$ and $n$ is a natural number defined as the infimum of the function that maps $s$ to the infimum of the function that maps $h$ to the cardinality of $s$.
Dynamics.dynEntouragedefMathlib.Dynamics.TopologicalEntropy.DynamicalEntourage, function or constantEnglish
Let $T$ be a function from elements of $X$ to elements of $X$. Let $U$ be a set relation of $X$ and $X$. Let $n$ be a natural number. Then $\operatorname{dynEntourage}$ applied to $T$, $U$ and $n$ is a set relation of $X$ and $X$ defined as the intersection of the function that maps $k$ to the intersection of the function that maps $h$ to the preimage of $\operatorname{iterate}$ applied to $\operatorname{map}$ applied to $T$ and $T$ and $k$ and $U$.
Dynamics.IsDynNetIndefMathlib.Dynamics.TopologicalEntropy.NetEntropy, predicateEnglish
Let $T$ be a function from elements of $X$ to elements of $X$. Let $F$ and $s$ be elements of $\wp X$. Let $U$ be a set relation of $X$ and $X$. Let $n$ be a natural number. Then $\operatorname{IsDynNetIn}$ holds for $T$, $F$, $U$, $n$ and $s$, if $s \leq F$ and $s$ is a pairwise disjoint with respect to the function that maps $x$ to the ball of $x$ and $\operatorname{dynEntourage}$ applied to $T$, $U$ and $n$.
Dynamics.netEntropyEntouragedefMathlib.Dynamics.TopologicalEntropy.NetEntropy, function or constantWording
the net entropy entourage of F and U (from the name)
English
Let $T$ be a function from elements of $X$ to elements of $X$. Let $F$ be an element of $\wp X$. Let $U$ be a set relation of $X$ and $X$. Then the net entropy entourage of $F$ and $U$ is an element of $\mathrm{EReal}$ defined as the exponential growth supremum of the function that maps $n$ to $\operatorname{toENNReal}$ applied to $\operatorname{netMaxcard}$ applied to $T$, $F$, $U$ and $n$.
Dynamics.netEntropyInfEntouragedefMathlib.Dynamics.TopologicalEntropy.NetEntropy, function or constantWording
the net entropy infimum entourage of F and U (from the name)
English
Let $T$ be a function from elements of $X$ to elements of $X$. Let $F$ be an element of $\wp X$. Let $U$ be a set relation of $X$ and $X$. Then the net entropy infimum entourage of $F$ and $U$ is an element of $\mathrm{EReal}$ defined as the exponential growth infimum of the function that maps $n$ to $\operatorname{toENNReal}$ applied to $\operatorname{netMaxcard}$ applied to $T$, $F$, $U$ and $n$.
Dynamics.netMaxcarddefMathlib.Dynamics.TopologicalEntropy.NetEntropy, function or constantEnglish
Let $T$ be a function from elements of $X$ to elements of $X$. Let $F$ be an element of $\wp X$. Let $U$ be a set relation of $X$ and $X$. Let $n$ be a natural number. Then $\operatorname{netMaxcard}$ applied to $T$, $F$, $U$ and $n$ is a natural number defined as the supremum of the function that maps $s$ to the supremum of the function that maps $h$ to the cardinality of $s$.
Dynamics.coverEntropySupBotHomdefMathlib.Dynamics.TopologicalEntropy.Subset, function or constantWording
the cover entropy supremum bottom homomorphism of T (from the name)
English
Let $T$ be a function from elements of $X$ to elements of $X$. Then the cover entropy supremum bottom homomorphism of $T$ is a supremum bottom homomorphism of $\wp X$ and $\mathrm{EReal}$ defined as $\operatorname{mk}$ applied to $\operatorname{mk}$ applied to $\operatorname{coverEntropy}$ applied to $T$ and the function that maps $x_{1}$ and $x_{2}$ to $\mathrm{Dynamics\_\_coverEntropy\_union}$ and $\mathrm{Dynamics\_\_coverEntropy\_empty}$.
AddAction.IsTopologicallyTransitiveclassMathlib.Dynamics.Transitive, predicateEnglish
Let $M$ and $x$ be sets. Then we can say that $\operatorname{IsTopologicallyTransitive}$ holds for $M$ and $x$.
MulAction.IsTopologicallyTransitiveclassMathlib.Dynamics.Transitive, predicateEnglish
Let $M$ and $x$ be sets. Then we can say that $\operatorname{IsTopologicallyTransitive}$ holds for $M$ and $x$.