Next:About this document ... Up:User's manual of the Previous:Basic definitions Contents

Compatible fonctions

$\begin{definition}[]~ \begin{center}% \afdmath{}\text{\rm Compatible}\hspace{0.2... ...Verb{Verb}Compatible f R\marginpar{\UseVerb{Verb}}\end{center}\end{definition}$

$\begin{definition}[]~ \begin{center}% \afdmath{}\text{\rm Lift}\hspace{0.2em} \t... ...SaveVerb{Verb}Lift f c z\marginpar{\UseVerb{Verb}}\end{center}\end{definition}$

$\begin{proposition}[% \afdmath{}\text{\rm lift}.\text{\rm compatible}.\text{\rm ... ...rettybox{}\endprettybox{}\right)\endprettybox{}\endafdmmath{} \end{proposition}$

$\begin{definition}[]~ \begin{center}% \afdmath{}\text{\rm lift}\hspace{0.2em} \t... ... \SaveVerb{Verb}lift f c\marginpar{\UseVerb{Verb}}\end{center}\end{definition}$

$\begin{proposition}[% \afdmath{}\text{\rm lift}.\text{\rm total}.\text{\rm Q}\en... ...rettybox{}\endprettybox{}\right)\endprettybox{}\endafdmmath{} \end{proposition}$

lift.total.Q added as introduction rule (abbrev: total , options: -c )

$\begin{proposition}[% \afdmath{}\text{\rm lift}.\text{\rm prop}\endafdmath{}]~ \... ...rettybox{}\endprettybox{}\right)\endprettybox{}\endafdmmath{} \end{proposition}$

lift.prop added as equation

$\begin{proposition}[% \afdmath{}\text{\rm class}.\text{\rm eq}.\text{\rm Q}\enda... ...}'\endprettybox{}\endprettybox{}\endprettybox{}\endafdmmath{} \end{proposition}$

About the axiom of choiceChristophe RaffalliParis VII & Paris XII university

$\begin{axiom}[% \afdmath{}\text{\rm AC}\endafdmath{}]~ \afdmmath{}\prettybox{}\f... ...xt{\it Q}\right)\endprettybox{}\right)\endprettybox{}\endafdmmath{} \end{axiom}$

$\begin{definition}[]~ \begin{center}% \afdmath{}\text{\rm Def}_{2_{1}}\hspace{0.... ... \SaveVerb{Verb}Def2_1 Q\marginpar{\UseVerb{Verb}}\end{center}\end{definition}$

$\begin{definition}[]~ \begin{center}% \afdmath{}\text{\rm Def}_{2_{2}}\hspace{0.... ... \SaveVerb{Verb}Def2_2 Q\marginpar{\UseVerb{Verb}}\end{center}\end{definition}$

$\begin{fact}[% \afdmath{}\text{\rm AC}2\endafdmath{}]~ \afdmmath{}\prettybox{}\f... ...ext{\it Q}\right)\endprettybox{}\right)\endprettybox{}\endafdmmath{} \end{fact}$

$\begin{definition}[]~ \begin{center}% \afdmath{}\text{\rm Chaine}\hspace{0.2em} ... ...veVerb{Verb}Chaine X R C\marginpar{\UseVerb{Verb}}\end{center}\end{definition}$

$\begin{theorem}[% \afdmath{}\text{\rm Zorn}\endafdmath{}]~ \afdmmath{}\prettybox... ...tybox{}\right)\endprettybox{}\right)\endprettybox{}\endafdmmath{} \end{theorem}$

$\begin{theorem}[% \afdmath{}\text{\rm Zermelo}\endafdmath{}]~ \afdmmath{}\pretty... ...}{2.em} \text{\it R}\endprettybox{}\endprettybox{}\endafdmmath{} \end{theorem}$

libudoc.ind

Christophe Raffalli 2005-03-02