Definitions: Mathlib.Logic, part 2 of 2

fiber of f (from the name)

Let $f$ be a function from elements of $Y$ to elements of $Z$. Then a fiber of $f$ is an element of the function that maps $f$ to the set of elements of the range of the function that maps $x$ to the preimage of $f$ and $\operatorname{singleton}$ applied to $x$.

the image of f and a (from the name)

Let $f$ be a function from elements of $Y$ to elements of $Z$. Let $a$ be a fiber of $f$. Then the image of $f$ and $a$ is an element of $Z$.

Let $f$ be a function from elements of $Y$ to elements of $Z$. Let $y$ be an element of $Y$. Then $\operatorname{mk}$ applied to $f$ and $y$ is a fiber of $f$ defined as the preimage of $f$ and $\operatorname{singleton}$ applied to $f$ applied to $y$.

the self of f and y (from the name)

Let $f$ be a function from elements of $Y$ to elements of $Z$. Let $y$ be an element of $Y$. Then the self of $f$ and $y$ is an element of $\operatorname{mk}$ applied to $f$ and $y$ defined as $y$.

the preimage of f and a (from the name)

Let $f$ be a function from elements of $Y$ to elements of $Z$. Let $a$ be a fiber of $f$. Then the preimage of $f$ and $a$ is an element of $Y$.

Let $x$ be a function from elements of $\mathrm{Fin}$ applied to $n$ to sets. Let $x_{1}$ be a set. Then an element of $\operatorname{FromTypes}$ applied to $x$ and $x_{1}$ is an element of the function that maps $x$ and $x_{1}$ to $\operatorname{brecOn}$ applied to $n$, $\mathrm{Function\_\_FromTypes\_\_\_f}$, $x$ and $x_{1}$.

the constant of p and t (from the name)

Let $p$ be a function from elements of $\mathrm{Fin}$ applied to $n$ to sets. Let $t$ be an element of $x$. Then the constant of $p$ and $t$ is an element of $\operatorname{FromTypes}$ applied to $p$ and $x$ defined as $\operatorname{brecOn}$ applied to $n$, $\mathrm{Function\_\_FromTypes\_\_const\_\_\_f}$, $p$, $x$ and $t$.

Let $x$ and $x_{1}$ be sets. Let $p$ be a function from elements of $\mathrm{Fin}$ applied to $n$ to sets. Then $\mathrm{Function\_\_fromTypes\_cons\_equiv}$ applied to $x$, $p$ and $x_{1}$ is an element of $\EquivMACRoAE {\operatorname{FromTypes} (\operatorname{vecCons} (x , p), x_{1})}{(\mathrm{Elem} (x)\rightarrow \operatorname{FromTypes} (p , x_{1}))}$ defined as $\mathrm{Function\_\_fromTypes\_succ\_equiv}$ applied to $\operatorname{vecCons}$ applied to $x$ and $p$ and $x_{1}$.

Let $x$ be a set. Then $\mathrm{Function\_\_fromTypes\_nil\_equiv}$ applied to $x$ is an element of $\EquivMACRoAE {\operatorname{FromTypes} (\operatorname{vecEmpty} , x)}{x}$ defined as $\mathrm{Function\_\_fromTypes\_zero\_equiv}$ applied to $\operatorname{vecEmpty}$ and $x$.

Let $p$ be a function from elements of $\mathrm{Fin}$ applied to $n + 1$ to sets. Let $x$ be a set. Then $\mathrm{Function\_\_fromTypes\_succ\_equiv}$ applied to $p$ and $x$ is an equivalence from $\operatorname{FromTypes}$ applied to $p$ and $x$ to the set of functions from elements of the vector head of $p$ to elements of $\operatorname{FromTypes}$ applied to $\operatorname{vecTail}$ applied to $p$ and $x$ defined as the identity of $\operatorname{FromTypes}$ applied to $p$ and $x$.

Let $p$ be a function from elements of $\mathrm{Fin}$ applied to $0$ to sets. Let $x$ be a set. Then $\mathrm{Function\_\_fromTypes\_zero\_equiv}$ applied to $p$ and $x$ is an element of $\EquivMACRoAE {\operatorname{FromTypes} (p , x)}{x}$ defined as the identity of $\operatorname{FromTypes}$ applied to $p$ and $x$.

Let $\mathrm{op}$ be a function from elements of $x$ to elements of $x$. Let $x_{1}$ be a natural number. Let $x_{2}$ be an element of $x$. Then $\operatorname{iterate}$ applied to $\mathrm{op}$, $x_{1}$ and $x_{2}$ is an element of $x$ defined as $\operatorname{brecOn}$ applied to $x_{1}$, $\mathrm{Nat\_\_iterate\_\_\_f}$ applied to $\mathrm{op}$ and $x_{2}$.

Let $x$ and $x_{1}$ be sets. Let $n$ be a natural number. Then $\mathrm{Function\_\_FromTypes\_\_fromTypes\_fin\_const\_equiv}$ applied to $x$, $x_{1}$ and $n$ is an equivalence from $\operatorname{FromTypes}$ applied to the function that maps $x_{2}$ to $x$ and $x_{1}$ to the set of arities of $x_{1}$ and $n$ defined as the identity of $\operatorname{FromTypes}$ applied to the function that maps $x_{2}$ to $x$ and $x_{1}$.

arity of x1 and n (from the name)

Let $x$ and $x_{1}$ be sets. Let $n$ be a natural number. Then an arity of $x_{1}$ and $n$ is an element of the function that maps $x$, $x_{1}$ and $n$ to $\operatorname{FromTypes}$ applied to the function that maps $x_{2}$ to $x$ and $x_{1}$.

the constant of b and n (from the name)

Let $x$ be a set. Let $b$ be an element of $x_{1}$. Let $n$ be a natural number. Then the constant of $b$ and $n$ is an arity of $x_{1}$ and $n$ defined as the constant of the function that maps $x_{2}$ to $x$ and $b$.

the Beta of n and i (from the name)

Let $n$ and $i$ be natural numbers. Then the Beta of $n$ and $i$ is a natural number defined as $\HModhModMACRoF {\ProdfstMACRoZ {\operatorname{unpair} (n)}}{((i + 1)\times \ProdsndMACRoAA {\operatorname{unpair} (n)}+ 1)}$.

Let $l$ be a list of natural numbers. Then $\operatorname{unbeta}$ applied to $l$ is a natural number.

Let $r$ be a function from elements of $x$ and elements of $x$ to propositions. Let $\mathrm{s'}$ and $s$ be multisets of $x$. Then $\operatorname{CutExpand}$ holds for $r$, $\mathrm{s'}$ and $s$, if there exists a multiset $t$ of $x$, such that there exists an element $a$ of $x$, such that for all elements $\mathrm{a'}$ of $x$, if $\mathrm{a'}$ is an element of $t$, then $r$ holds for $\mathrm{a'}$ and $a$ and $\EqtMACRoH {\mathrm{s'} + \operatorname{singleton} (a)}{s + t}$.

op is a inverse opposite (from the name)

Let $\mathrm{op}$ be a function from elements of $x$ and elements of $x$ to elements of $x_{1}$. Then we can say that $\mathrm{op}$ is an inverse opposite.

Let $\mathrm{op}$ be a function from elements of $x$ and elements of $x_{1}$ to elements of $x_{1}$. Then we can say that $\mathrm{LeftCommutative}$ holds for $\mathrm{op}$.

Let $\mathrm{op}$ be a function from elements of $x_{1}$ and elements of $x$ to elements of $x_{1}$. Then we can say that $\mathrm{RightCommutative}$ holds for $\mathrm{op}$.

r is pairwise (from the name)

Let $r$ be a function from elements of $x$ and elements of $x$ to propositions. Then $r$ is pairwise, if for all elements $i$ and $j$ of $x$, if $i \neq j$, then $r$ holds for $i$ and $j$.

Let $s$ be an element of $\wp x$. Let $r$ be a function from elements of $x$ and elements of $x$ to propositions. Then $\operatorname{Pairwise}$ holds for $s$ and $r$, if for all elements $x_{1}$ of $x$, if $x_{1}$ is an element of $s$, then for all elements $y$ of $x$, if $y$ is an element of $s$, then if $x_{1} \neq y$, then $r$ holds for $x_{1}$ and $y$.

Let $r$ be a function from elements of $x$ and elements of $x_{1}$ to propositions. Let $p$ be a function from elements of $x_{1}$ and elements of $x_{2}$ to propositions. Let $a$ be an element of $x$. Let $c$ be an element of $x_{2}$. Then $\operatorname{Comp}$ holds for $r$, $p$, $a$ and $c$, if there exists an element $b$ of $x_{1}$, such that $r$ holds for $a$ and $b$ and $p$ holds for $b$ and $c$.

Let $r$ be a function from elements of $x$ and elements of $x$ to propositions. Let $x_{1}$ and $x_{2}$ be elements of $x$. Then we can say that $\operatorname{EqvGen}$ holds for $r$, $x_{1}$ and $x_{2}$.

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

Let $x_{2}$ be a function from elements of $x$ and elements of $x$ to propositions. Let $x_{3}$ be a function from elements of $x_{1}$ and elements of $x_{1}$ to propositions. Let $f$ be a function from elements of $x$ to elements of $x_{1}$. Then $\operatorname{Fibration}$ holds for $x_{2}$, $x_{3}$ and $f$, if for all elements $a$ of $x$, for all elements $b$ of $x_{1}$, if $x_{3}$ holds for $b$ and $f$ applied to $a$, then there exists an element $\mathrm{a'}$ of $x$, such that $x_{2}$ holds for $\mathrm{a'}$ and $a$ and $\EqtMACRoH {f (\mathrm{a'})}{b}$.

Let $r$ be a function from elements of $x$ and elements of $x$ to propositions. Let $x_{1}$ and $x_{2}$ be elements of $x$. Then $\operatorname{Join}$ holds for $r$, $x_{1}$ and $x_{2}$, if there exists an element $c$ of $x$, such that $r$ holds for $x_{1}$ and $c$ and $r$ holds for $x_{2}$ and $c$.

Let $r$ be a function from elements of $x$ and elements of $x_{1}$ to propositions. Let $f$ be a function from elements of $x$ to elements of $x_{2}$. Let $g$ be a function from elements of $x_{1}$ to elements of $x_{3}$. Let $x_{4}$ be an element of $x_{2}$. Let $x_{5}$ be an element of $x_{3}$. Then $\operatorname{Map}$ holds for $r$, $f$, $g$, $x_{4}$ and $x_{5}$, if there exists an element $a$ of $x$, such that there exists an element $b$ of $x_{1}$, such that $r$ holds for $a$ and $b$, $\EqtMACRoH {f (a)}{x_{4}}$ and $\EqtMACRoH {g (b)}{x_{5}}$.

Let $r$ be a function from elements of $x$ and elements of $x$ to propositions. Let $a$ and $x_{1}$ be elements of $x$. Then we can say that $\operatorname{ReflGen}$ holds for $r$, $a$ and $x_{1}$.

Let $r$ be a function from elements of $x$ and elements of $x$ to propositions. Let $a$ and $x_{1}$ be elements of $x$. Then we can say that $\operatorname{ReflTransGen}$ holds for $r$, $a$ and $x_{1}$.

Assume that $\operatorname{ReflTransGen}$ holds for $r$, $a$ and $x_{1}$. Then we can say that $\operatorname{below}$ holds for $t$.

Let $r$ be a function from elements of $x$ and elements of $x$ to propositions. Let $a$ and $b$ be elements of $x$. Then $\operatorname{SymmGen}$ holds for $r$, $a$ and $b$, if $r$ holds for $a$ and $b$ or $r$ holds for $b$ and $a$.

Let $R$ be a function from elements of $x$ and elements of $x_{1}$ to propositions. Then $\operatorname{BiTotal}$ holds for $R$, if $\operatorname{LeftTotal}$ holds for $R$ and $\operatorname{RightTotal}$ holds for $R$.

Let $R$ be a function from elements of $x$ and elements of $x_{1}$ to propositions. Then $\operatorname{BiUnique}$ holds for $R$, if $\operatorname{LeftUnique}$ holds for $R$ and $\operatorname{RightUnique}$ holds for $R$.

Let $R$ be a function from elements of $x$ and elements of $x_{1}$ to propositions. Then $\operatorname{LeftTotal}$ holds for $R$, if for all elements $a$ of $x$, there exists an element $b$ of $x_{1}$, such that $R$ holds for $a$ and $b$.

Let $R$ be a function from elements of $x$ and elements of $x_{1}$ to propositions. Then $\operatorname{LeftUnique}$ holds for $R$, if for all elements $a$ and $b$ of $x$, for all elements $c$ of $x_{1}$, if $R$ holds for $a$ and $c$, then if $R$ holds for $b$ and $c$, then $\EqtMACRoH {a}{b}$.

Let $R$ be a function from elements of $x$ and elements of $x_{1}$ to propositions. Let $S$ be a function from elements of $x_{2}$ and elements of $x_{3}$ to propositions. Let $f$ be a function from elements of $x$ to elements of $x_{2}$. Let $g$ be a function from elements of $x_{1}$ to elements of $x_{3}$. Then $\operatorname{LiftFun}$ holds for $R$, $S$, $f$ and $g$, if for all elements $a$ of $x$, for all elements $b$ of $x_{1}$, if $R$ holds for $a$ and $b$, then $S$ holds for $f$ applied to $a$ and $g$ applied to $b$.

Let $R$ be a function from elements of $x$ and elements of $x_{1}$ to propositions. Then $\operatorname{RightTotal}$ holds for $R$, if for all elements $b$ of $x_{1}$, there exists an element $a$ of $x$, such that $R$ holds for $a$ and $b$.

Let $R$ be a function from elements of $x$ and elements of $x_{1}$ to propositions. Then $\operatorname{RightUnique}$ holds for $R$, if for all elements $a$ of $x$, for all elements $b$ and $c$ of $x_{1}$, if $R$ holds for $a$ and $b$, then if $R$ holds for $a$ and $c$, then $\EqtMACRoH {b}{c}$.

shrink of x (from the name)

Let $x$ be a set. Then a shrink of $x$ is an element of the function that maps $x$ to $\operatorname{choose}$ applied to $\mathrm{Small\_\_equiv\_small}$.

x is small (from the name)

Let $x$ be a set. Then we can say that $x$ is small.

the equivalence shrink of x (from the name)

Let $x$ be a set. Then the equivalence shrink of $x$ is an equivalence from $x$ to the set of shrinks of $x$.