Maths Discrètes Licence 1
--- Introduction ---
|
Ce module regroupe 402 exercices
à destination des étudiants de première année du portail
Sciences Fondamentales de l'Université de Nice Sophia Antipolis
|
1 Evaluer (deux quantif. réels) le vrai
Calculer :
1 Evaluer (deux quantif. réels) vrai V29
Calculer :
1 Evaluer (table de vérité) backup
Ecrire la table de vérité de
1 Evaluer (table de vérité) V20? backup
Ecrire la table de vérité de
1 NewNier finit positive backup
Ici
est une fonction. Nier :
1 NewNier finit positive vrai
Ici
est une fonction. Nier :
1 Traduire (fonctions) V60? backup
(Choisissez -- si l'énoncé ne dit rien.)
2 Evaluer suites II
Dites si l'énoncé suivant est vrai ou faux
.
2 Evaluer suites II exam
Dites si l'énoncé suivant est vrai ou faux
.
2 Formaliser CNCS(nb) V30? backup
2 Formaliser CNCS(nb) V30?backup
2 Formaliser CNCS(nb) V30?exam
Au choix, on privilégiera l'ordre alphabétique.
444 Carré de majorée
444 Constante implique majorée
444 Double de surjective
444 Cinq gratuites
Donner une liste de cinq tactiques gratuites qui s'applique au but suivant [on fera le minimum au contexte pour pouvoir agir au but, on sautera les explicitations, et s'il reste du choix on privilégiera l'ordre alphabétique des tactiques] Si une suite finit arithmétique ses multiples aussi
444 Cinq gratuites rapides
Donner une liste de cinq tactiques gratuites qui s'applique au but suivant [on fera le minimum au contexte pour pouvoir agir au but, on sautera les explicitations, et s'il reste du choix on privilégiera l'ordre alphabétique des tactiques] La somme de deux suites qui finissent constantes finit constante
444 Constante implique bornée
444 Opposée de Cauchy
444 valabs majorée implique bornée
444 Double de constante backup
444 Double de constante vrai
444 Double de surjective backup
444 Maximum de constante
444 Maximum de constante backup
444 Nb de var
On essaie de prouver l'énoncé : Toute fonction dont le carré est majoré est elle-même majorée en appliquant autant que possible les tactiques gratuites ImpB EtC EtB OuB OuC ForallB ExistsC. Une fois que c'est fait, combien le contexte courant contient-il de variables libres?
444 Nb de var 2
On essaie de prouver l'énoncé : Si une fonction est majorée il en est de même pour tous ses multiples en appliquant autant que possible les tactiques gratuites ImpB EtC EtB OuB OuC ForallB ExistsC. Une fois que c'est fait, combien le contexte courant contient-il de variables libres?
444 Nb de var 3
On essaie de prouver l'énoncé : Si une fonction est monotone il en est de même pour tous ses multiples en appliquant autant que possible les tactiques gratuites ImpB EtC EtB OuB OuC ForallB ExistsC. Une fois que c'est fait, combien le contexte courant contient-il de variables libres?
444 Nb de var 4
On essaie de prouver l'énoncé : Toute combinaison linéaire de deux fonctions bornées est bornée en appliquant autant que possible les six tactiques gratuites EtC EtB OuB OuC ForallB ExistsC. Une fois que c'est fait, combien le contexte courant contient-il de variables?
444 Qui atteint ses bornes est majorée
4 Opposée de surjective
test2 Affine et surjective
test1 tacgrat6
444 Affine et injective
test2 Double de constante exam
test2 Associativité de la réunion
Donner les premières tactiques qu'il vous faut exécuter pour prouver
.
[Attention, OuB désigne le Ou faible (non gratuit)].
test1 tacgrat5
644 constante et affine
644 finit affine et multiples
644 finit periodique et multiples
644 finit surjective et surjective
644 finit surjective pas injective
744 BBconstante implique majorée
744 Carré de majorée 1
744 Double de bconstante
744 Double de finit surjective
744 Maximum de bconstante
745 BBconstante implique CCconstante
745 constante implique BBconstante
AAAABmax_des partiest
Voici un énoncé suivi d'un début de preuve en étapes:
Toute partie non-vide et majorée de
admet un plus grand élément. Preuve. 1- On montre par récurrence sur n que toute partie P de
non-vide et majorée par n admet un plus grand élément.
2- Si n est nul, alors le maximum de P est O.
3- Soit maintenant P une partie non-vide et majorée par n+1. Si n+1 est dans P, c'en est forcément le plus grand élément.
4- Si au contraire n+1 n'est pas dans P, l'hypothèse de récurrence s'applique: en effet, dans ce cas, P est en fait majoré par n.
Avec les blocs proposés ci-dessous, formez la liste de tactiques proposées par cette preuve (à l'exclusion de celles qui traitent les buts sur lesquels la preuve est muette).
AAAA Croissance du Max 5
Voici le même énoncé suivi en étapes:
Avec les blocs proposés ci-dessous, formez
AAAAFVImageRecInter
AAAAImMonot3t
Voici le même énoncé suivi en étapes:
Avec les blocs proposés ci-dessous, formez
AAAA L'intersection est commutative
Donner les tactiques qu'il vous faut exécuter pour prouver
.
[Attention, OuB désigne le Ou faible (non gratuit)].
AAAATac convergente plus stationnaire
AAAAYG Associativité de la réunion
Donner les premières tactiques qu'il vous faut exécuter pour prouver
.
[Attention, OuB désigne le Ou faible (non gratuit)].
2 Evaluer (fonctions) V50?
Dites si l'énoncé suivant est vrai ou faux
Privilégier le contexte entrainement
AA Croissance de l'intersec Tac
Donner les tactiques qu'il vous faut exécuter pour prouver
.
[Attention, OuB désigne le Ou faible (non gratuit)].
AA Intersection idem
Donner les tactiques qu'il vous faut exécuter pour prouver
.
[Attention, OuB désigne le Ou faible (non gratuit)].
AA Monotonie complementaire Tac
Donner les tactiques qu'il vous faut exécuter pour prouver
.
[Attention, OuB désigne le Ou faible (non gratuit)].
Aide: La 10. tactique est Contrapos.
AA Reunion idem
Donner les tactiques qu'il vous faut exécuter pour prouver
.
[Attention, OuB désigne le Ou faible (non gratuit)].
Témoigner (fonctions) V15
essaie de prouver l'énoncé . Il a appliqué la liste suivante de tactiques avec les variables et arguments indiqués. Pourra-t-il s'en sortir ?
AA vide absorbant
Donner les tactiques qu'il vous faut exécuter pour prouver
.
[Attention, OuB désigne le Ou faible (non gratuit)].
AA vide neutre2
Donner les tactiques qu'il vous faut exécuter pour prouver
.
[Attention, OuB désigne le Ou faible (non gratuit)].
XC Définir croissance fonctions V 4
AE0
AE1
Voici le même énoncé suivi en étapes:
Avec les blocs proposés ci-dessous, formez
AE2
Voici le même énoncé suivi en étapes:
Avec les blocs proposés ci-dessous, formez
AE3
Voici le même énoncé suivi en étapes:
Avec les blocs proposés ci-dessous, formez
AE4
Voici le même énoncé suivi en étapes:
Avec les blocs proposés ci-dessous, formez
AE5
Voici le même énoncé suivi en étapes:
Avec les blocs proposés ci-dessous, formez
A Evaluer (deux quantif. réels) 1
Calculer :
Evaluer (deux quantif. réels) V30?
Calculer :
Evaluer (deux quantificateurs entiers) V
Calculer :
Evaluer (fonctions) V3
Dites si l'énoncé suivant est vrai ou faux
Evaluer réels ou complexes v5
Evaluer (sans quantificateur) V25?
Calculer :
Formaliser CNCS(nb) V30?
Formaliser fonctions I V2
Formalisez l'énoncé : .
Formaliser fonctions II V2
Formalisez l'énoncé : .
Formaliser (nb nonamb) V12?
XC Inférer le contexte (fonctions) V3
Témoigner meilleur temooin
Dans le contexte
, Bob s'attaque au but
, Il propose la tactique ExistB. Parmi ceux que Bob envisage, quel est le meilleur témoin?
Témoin choisir le bon
Bob essaie de prouver l'énoncé
Pour qu'une fonction soit majorée il suffit que son double le soit. Il a appliqué la liste suivante de tactiques avec les variables et arguments indiqués.
ForallB [f] ImpB ReecC ExistC[M] ReecB Il va maintenant appliquer ExistB et il hésite pour le témoin. Quel est le bon choix?
XC Variables libres (formules) V30
Dans la formule suivante, identifier les variables libres.
(ATTENTION: Séparez vos variables par des virgules. Tapez VIDE si la liste de variables répondant à la question est vide. Le comparateur distingue les majuscules des minuscules.)
XC Variables libres (Enoncés) V30
Dans l'énoncé suivant, identifier les variables libres.
(ATTENTION: Séparez vos variables par des virgules. Tapez VIDE si la liste de variables répondant à la question est vide. Le comparateur distingue les majuscules des minuscules.)
Formaliser CNCS(nb) V30?
Formaliser (nb nonamb) V12?
AH Cinq tactiques
AH Huit tactiques fonctions
AH ImRecDiff0
AH ImRecDiff1g
Voici le même énoncé suivi en étapes:
Avec les blocs proposés ci-dessous, formez
AH ImRecDiff1t
Voici le même énoncé suivi en étapes:
Avec les blocs proposés ci-dessous, formez
AH ImRecDiff2g
Voici le même énoncé suivi en étapes:
Avec les blocs proposés ci-dessous, formez
AH ImRecDiff2t
Voici le même énoncé suivi en étapes:
Avec les blocs proposés ci-dessous, formez
AH ImRecDiff3g
Voici le même énoncé suivi en étapes:
Avec les blocs proposés ci-dessous, formez
AH ImRecDiff3t
Voici le même énoncé suivi en étapes:
Avec les blocs proposés ci-dessous, formez
AH ImRecDiff4g
Voici le même énoncé suivi en étapes:
Avec les blocs proposés ci-dessous, formez
AH ImRecDiff4t
Voici le même énoncé suivi en étapes:
Avec les blocs proposés ci-dessous, formez
AH ImRecDiff5g
Voici le même énoncé suivi en étapes:
Avec les blocs proposés ci-dessous, formez
AH ImRecDiff5t
Voici le même énoncé suivi en étapes:
Avec les blocs proposés ci-dessous, formez
AH ImRecDiff6t
Voici le même énoncé suivi en étapes:
Avec les blocs proposés ci-dessous, formez
AH Infos
Les exercices suivants concerne la différence, qui est une opération sur les parties d'un ensemble, comme l'intersection et la réunion. Si P et Q sont deux parties de l'ensemble X, la différence P-Q est constituée des éléments de X qui sont dans P mais pas dans Q.
Par exemple pour X :=R, P := [1,3] et Q := [2, 6], on a P-Q = [1, 2[ et Q-P = ]3, 6].
La règle de réécriture correspondante est donc
Par ailleurs, notez que les buts intermédiaires sont mieux payés (poids 3) que les tactiques. Traîtez-les donc avec le plus grand soin. Aussi, si vous vous trompez sur les buts intermédiaires, wims vous les donne: notez-les soigneusement pour la suite.
Pour sortir de cet "exo", tapez ok, si vous préférez le vert.
AH Preuves fonctions, 6,7,8
AH Privilégier le contexte memes tac
AH Six tactiques SuiteEtFin
2 Evaluer réels ou complexes v55
Typer (réels ou complexes) V20
Evaluer (table de vérité) secours
Ecrire la table de vérité de
Evaluer (deux quantificateurs entiers) V
Calculer :
Evaluer (deux quantif. réels) V30?
Calculer :
1 Evaluer (fonctions) V50
Dites si l'énoncé suivant est vrai ou faux
.
Evaluer réels ou complexes v50?
Evaluer (sans quantificateur) V25?
Calculer :
Evaluer (table de vérité) V20?
Ecrire la table de vérité de
Evaluer (table de vérité) secours
Ecrire la table de vérité de
Tac 5 Finit V25
2 Formaliser CNCS(nb) V30?
Formaliser fonctions I
Formalisez l'énoncé : .
2 Formaliser fonctions genre majorées V
Formalisez l'énoncé : .
Formaliser (nb nonamb) V12?
XC Inférer le contexte (fonctions) V7
Témoigner x ou 2y
Dans le contexte
Bob s'attaque au but
Il propose la tactique ExistB avec pour témoin
Pourra-t-il s'en sortir? (y/n)
Témoigner (fonctions) test
Bob essaie de prouver l'énoncé
. Il a appliqué la liste suivante de tactiques avec les variables et arguments indiqués.
Peut-il encore s'en sortir? (y/n)
Variables libres (énoncés) V30
Dans l'énoncé suivant, identifier les variables libres.
(ATTENTION: Séparez vos variables par des virgules. Tapez VIDE si la liste de variables répondant à la question est vide. Le comparateur distingue les majuscules des minuscules.)
Variables libres (formules) V30
Dans l'énoncé suivant, identifier les variables libres.
(ATTENTION: Séparez vos variables par des virgules. Tapez VIDE si la liste de variables répondant à la question est vide. Le comparateur distingue les majuscules des minuscules.)
Archimède 1
Voici un énoncé trouvé sur le web (www.math.univ-toulouse.fr/~yak/Suites-Poly.pdf , p.8), suivi de son début de preuve :
Preuve. ...
Avec les blocs proposés ci-dessous, formez la liste de tactiques suggérée par ce début de preuve. On mettra Facile pour traîter chaque séquent pour lequel la preuve fournie ne donne aucune indication.
YH L'intersection est commutative bis
Donner les tactiques qu'il vous faut exécuter pour prouver
.
Archimède 3
Voici un énoncé trouvé sur le web (www.math.univ-toulouse.fr/~yak/Suites-Poly.pdf , p.8), suivi de sa preuve :
Preuve.
Avec les blocs proposés ci-dessous, formez la liste de tactiques suggérée par cette dernière phrase de la preuve. On mettre Facile pour traîter chaque séquent pour lequel la preuve fournie ne donne aucune indication.
BL Croissance du Max 0
BL Croissance du Max 1
Voici le même énoncé suivi en étapes:
Avec les blocs proposés ci-dessous, formez
BL Croissance du Max 2
Voici le même énoncé suivi en étapes:
Avec les blocs proposés ci-dessous, formez
BL Croissance du Max 3
Voici le même énoncé suivi en étapes:
Avec les blocs proposés ci-dessous, formez
BL Croissance du Max 4
Voici le même énoncé suivi en étapes:
Avec les blocs proposés ci-dessous, formez
BL Croissance du Max 5
Voici le même énoncé suivi en étapes:
Avec les blocs proposés ci-dessous, formez
BMaxCroissantAlpha
Voici un énoncé:
Si P et Q sont deux parties non-vides et majorées de
avec P contenue dans Q alors on a max P
max Q.
Et le début de "preuve" de Bob:
Ress, Ress, ForallB, ForallB, ImpB, EtC, EtC, EtC, EtC, ReecC, ForallC, EtC, ForallC, EtC, ForallC, ImpC
Bob s'est presque sûrement trompé et en plus il a oublié de privilégier l'ordre alphabétique. Avec les blocs proposés ci-dessous, remettez dans l'ordre la partie correcte de sa preuve.
BMaxCroissantBob
Voici un énoncé:
Si P et Q sont deux parties non-vides et majorées de
avec P contenue dans Q alors on a max P
max Q.
Et le début de "preuve" de Bob:
Ress, Ress, ForallB, ForallB, ImpB, EtC, EtC, EtC, EtC, ReecC, ForallC, EtC, ForallC, EtC, ForallC, ImpC
Bob s'est presque sûrement trompé. Avec les blocs proposés ci-dessous, recopiez la partie correcte de sa preuve.
BMaxReu
Voici un énoncé:
Le maximum de la réunion de deux parties non-vides et majorées de
est le plus grand des deux maxima.
Et le début de "preuve" de Bob:
Ress, Ress, ForallB, ForallB, ImpB, EtC, EtC, EtC, ReecC, ReecC, ReecC, ReecC, ForallC, ForallC, EtC, EtC, ReecB
Bob s'est peut-être trompé et en plus il a oublié de privilégier l'ordre alphabétique. Avec les blocs proposés ci-dessous, remettez dans l'ordre la partie correcte de sa preuve.
Bmax_des partiesg
Voici un énoncé suivi d'un début de preuve en étapes:
Toute partie non-vide et majorée de
admet un plus grand élément. Preuve. 1- On montre par récurrence sur n que toute partie P de
non-vide et majorée par n admet un plus grand élément.
2- Si n est nul, alors 0 est le plus grand élément de P.
3- Soit maintenant P une partie non-vide et majorée par n+1. Si n+1 est dans P, c'en est forcément le plus grand élément.
4- Si au contraire n+1 n'est pas dans P, alors P est en fait majoré par n et l'hypothèse de récurrence s'applique.
Avec les blocs proposés ci-dessous, formez le but intermédiaire
Bmax_des partiest
Voici un énoncé suivi d'un début de preuve en étapes:
Toute partie non-vide et majorée de
admet un plus grand élément. Preuve. 1- On montre par récurrence sur n que toute partie P de
non-vide et majorée par n admet un plus grand élément.
2- Si n est nul, alors le maximum de P est O.
3- Soit maintenant P une partie non-vide et majorée par n+1. Si n+1 est dans P, c'en est forcément le plus grand élément.
4- Si au contraire n+1 n'est pas dans P, l'hypothèse de récurrence s'applique: en effet, dans ce cas, P est en fait majoré par n.
Avec les blocs proposés ci-dessous, formez la liste de tactiques proposées par cette preuve (à l'exclusion de celles qui traitent les buts sur lesquels la preuve est muette).
Témoigner x2 et y
Dans le contexte s'attaque au but Il propose la tactique ExistB avec pour témoin Pourra-t-il s'en sortir ?
XC Inférer le contexte (fonctions) V20
Croissante majorée 1
Voici un énoncé trouvé sur le web (www.math.univ-toulouse.fr/~yak/Suites-Poly.pdf , p.25), suivi de son début de preuve :
Preuve.
La deuxième phrase ci-dessus suggère une liste de tactiques dont vous devez donner seulement la première et la dernière.
Croissante majorée 1bis
Voici un énoncé trouvé sur le web (www.math.univ-toulouse.fr/~yak/Suites-Poly.pdf , p.25), suivi de son début de preuve :
Preuve.
La deuxième phrase ci-dessus suggère une liste de tactiques dont vous devez donner seulement les trois premières et les deux dernières (avec "..." après les trois premières)..
DQuestion 0
DQuestion 1
DQuestion 2
DQuestion 3
DQuestion 4
Début gratuit 1
1 Définition et négation (Xiao)
Soit
une fonction réelle.
Formalisez la propriété ``
est ''. (Tirez les éléments pour composer votre formule)
La propriété ``
est '' se formalise en .
Quel est le contraire (négation) de cette propriété ?
Maintenant formalisez la négation ``
n'est pas ''.
La négation ``
n'est pas '' se formalise donc en . Donnez deux valeurs
,
pour montrer que la fonction ci-contre n'est pas , selon la formule. (Chaque case de la grille vaut 1 ; il faut donc choisir
et
entre -5 et 5.)
Densité 1
Voici un énoncé trouvé sur le web (www.math.univ-toulouse.fr/~yak/Suites-Poly.pdf , p.8), suivi de son début de preuve :
est dense dans
Preuve. Comme
est archimédien, il existe un entier q > 0 tel que 1/(y − x) < q ainsi qu’un entier n > 0 tel que qx < n...
Avec les blocs proposés ci-dessous, formez la liste de tactiques suggérée par ce début de preuve. On privilégiera l'ordre alphabétique des tactiques.
Densité 1bis
Voici un énoncé trouvé sur le web (www.math.univ-toulouse.fr/~yak/Suites-Poly.pdf , p.8), suivi de son début de preuve :
est dense dans
Preuve. Comme
est archimédien, il existe un entier q > 0 tel que 1/(y − x) < q ainsi qu’un entier n > 0 tel que qx < n...
Avec les blocs proposés ci-dessous, formez la liste de tactiques suggérée par ce début de preuve. On privilégiera l'ordre alphabétique des tactiques.
Densité2
Voici un énoncé trouvé sur le web (www.math.univ-toulouse.fr/~yak/Suites-Poly.pdf , p.8), suivi de son début de preuve :
est dense dans
Preuve. Comme
est archimédien, il existe un entier q > 0 tel que 1/(y − x) < q ainsi qu’un entier n > 0 tel que qx < n . Comme l’ensemble
est minoré par 1 et contient n, il possède un minimum qu'on note p.
Avec les blocs proposés ci-dessous, formez la liste de tactiques suggérée par la deuxième phrase de cette preuve. On privilégiera l'ordre alphabétique des tactiques.
Densité3
Voici un énoncé trouvé sur le web (www.math.univ-toulouse.fr/~yak/Suites-Poly.pdf , p.8), suivi de sa preuve :
est dense dans
Preuve. Comme
est archimédien, il existe un entier q > 0 tel que 1/(y − x) < q ainsi qu’un entier n > 0 tel que qx < n . Comme l’ensemble
est minoré par 1 et contient n, il possède un minimum qu'on note p. On a donc p − 1 ≤ qx < p de sorte que qx < p ≤ qx + 1 et x < p/q ≤ x + 1/q < y par la première inégalité.
La fin de la preuve est incorrecte. A partir de la liste des inégalités prétendues, formez la liste des inégalités prouvables . On les laissera dans l'ordre proposé ci-dessous.
1 Formaliser croissance fonctions V 4
EQuestion 0
EQuestion 1
EQuestion 2
EQuestion 3
EQuestion 4
EQuestion 5
1 Formaliser CNCScroissance fonctions V6
1 Evaluer (deux quantif. réels) V29
Calculer :
1 Evaluer (sans quantificateur) V28
Calculer :
1 Evaluer (deux quants entiers) V50
Calculer :
2 Evaluer suites II vieux
Dites si l'énoncé suivant est vrai ou faux
.
Tac 8 V22
Formaliser fonctions II
Formalisez l'énoncé : .
Formaliser fonctions I
Formalisez l'énoncé : .
Tac 8 fonctions V12
Tac 5 fini V17
Tac SuiteEtFin V12
XF Preuve guidée fonctions
2 Evaluer suites I
Dites si l'énoncé suivant est vrai ou faux
.
XC Formaliser suites V6
Formalisez l'énoncé : .
Former une CNouS mijo
Tac Composition graphes the old one
FT Applipart phrase 1
Tac convergente plus stationnaire
Tac stationnaire plus stationnaire
FT Tactiques finales
FT Objectifs finaux
FT Applipart la fin
FT Applipart phrase 2
FT Applipart phrase 3
FT Applipart phrase 1
FT Applipart phrase 1
FT Applipart phrase 1
FT Formaliser
FU Formaliser
FUReltot phrase 1
FUReltot phrase 2
FUReltot phrase 3
FVImageInter
FVImageInterGen
FVImageRecCompl
FVImageRecInter
FVImageRecReu
FVImageReu
FVRecip
FVRecip0
2 Définir nier majminbor fonctions V3x2
. Formalisez l'énoncé : .
1 Formaliser CNCS mijo fonctions V25
1 Traduire (fonctions) V60?
(Choisissez -- si l'énoncé ne dit rien.)
PreuveGen0
Définir inj V1
. Formalisez l'énoncé : .
2 Définir surj V4
. Formalisez l'énoncé : .
2 Définir pairimpperconst V4
. Formalisez l'énoncé : .
2 Former CS (suites mijo) V30
2 Former une CN mijo V50
ImInter2
ImInter3
ImInterDer
Voici maintenant l'énoncé suivi de sa preuve complète:
Preuve.
Avec les blocs proposés ci-dessous, formez la liste de tactiques suggérée par le dernier alinéa de cette preuve.
ImMonot0
ImMonot1g
Voici le même énoncé suivi en étapes:
Avec les blocs proposés ci-dessous, formez
ImMonot1t
Voici le même énoncé suivi en étapes:
Avec les blocs proposés ci-dessous, formez
ImMonot2g
Voici le même énoncé suivi en étapes:
Avec les blocs proposés ci-dessous, formez
ImMonot2t
Voici le même énoncé suivi en étapes:
Avec les blocs proposés ci-dessous, formez
ImMonot3t
Voici le même énoncé suivi en étapes:
Avec les blocs proposés ci-dessous, formez
ImRecCompl0
ImRecCompl1g
Voici le même énoncé suivi d'un début de preuve en étapes:
Preuve.
Avec les blocs proposés ci-dessous, formez
ImRecCompl2g
Voici le même énoncé suivi d'un début de preuve en étapes:
Preuve.
Avec les blocs proposés ci-dessous, formez
ImRecCompl2t
Voici le même énoncé suivi d'un début de preuve en étapes:
Preuve.
Avec les blocs proposés ci-dessous, formez
ImRecMonot2t
Voici le même énoncé suivi d'une preuve en étapes:
Preuve.
Avec les blocs proposés ci-dessous, formez
ImRecCompl3g
Voici le même énoncé suivi d'un début de preuve en étapes:
Preuve.
Avec les blocs proposés ci-dessous, formez
ImRecCompl3t
Voici le même énoncé suivi d'un début de preuve en étapes:
Preuve.
Avec les blocs proposés ci-dessous, formez
ImRecCompl4t
Voici le même énoncé suivi d'un début de preuve en étapes:
Preuve.
Avec les blocs proposés ci-dessous, formez
ImRecInter0
ImRecInter1
ImRecInter2
ImRecInter3
ImRecInterDer
Voici maintenant l'énoncé suivi de sa preuve complète:
Preuve.
Avec les blocs proposés ci-dessous, formez la liste de tactiques suggérée par le dernier alinéa de cette preuve.
ImRecMonot0
ImRecMonot1g
Voici le même énoncé suivi d'une preuve en étapes:
Preuve.
Avec les blocs proposés ci-dessous, formez
PreuveGen1t
Voici le même énoncé suivi en étapes:
Avec les blocs proposés ci-dessous, formez
ImRecMonot1t
Voici le même énoncé suivi en étapes:
Avec les blocs proposés ci-dessous, formez
ImRecMonot2g
Voici le même énoncé suivi d'une preuve en étapes:
Preuve.
Avec les blocs proposés ci-dessous, formez
ImRecMonot3t
Voici le même énoncé suivi d'une preuve en étapes:
Preuve.
Avec les blocs proposés ci-dessous, formez
ImRecMonotINV
ImReu0
ImReu1
ImReu2
ImReu3
ImReu4
ImReu5
ImInter0
ImInter1
La composée de deux fonctions dont l'une
Voici un énoncé :
La composée de deux fonctions dont l'une est constante est elle-même constante.
Vous devez concevoir un enchainement de tactiques prouvant cet énoncé, et donner le sous-enchaînement correspondant de tactiques Forall et Exist. Vous devez choisir une preuve conduisant à la réponse optimale du point de vue de l'ordre alphabétique inverse.
BMaxCroissantLibre
Voici un énoncé suivi d'un début de preuve:
Si P et Q sont deux parties non-vides et majorées de
avec P contenue dans Q alors on a max P
max Q.
Avec les blocs proposés ci-dessous, formez une preuve qui commence par invoquer deux fois la ressource.
Modele de preuve
Donner les tactiques de votre preuve du but suivant
PreuveGen2g
Voici le même énoncé suivi en étapes:
Avec les blocs proposés ci-dessous, formez
PreuveGen2t
Voici le même énoncé suivi en étapes:
Avec les blocs proposés ci-dessous, formez
PreuveGen4t
Voici le même énoncé suivi en étapes:
Avec les blocs proposés ci-dessous, formez
PreuveGen3t
Voici le même énoncé suivi en étapes:
Avec les blocs proposés ci-dessous, formez
PreuveGen5t
Voici le même énoncé suivi en étapes:
Avec les blocs proposés ci-dessous, formez
PreuveGen1g
Voici le même énoncé suivi en étapes:
Avec les blocs proposés ci-dessous, formez
ImRecCompl1t
Voici le même énoncé suivi d'un début de preuve en étapes:
Preuve.
Avec les blocs proposés ci-dessous, formez
PreuveParties AuB dans B
Donner les tactiques de votre preuve du but suivant
PreuveParties A dans AnB contexte vrai
Donner les tactiques de votre preuve du but suivant en sous-entendant les réécritures et
PreuveParties AuB dans B au contexte
Donner les tactiques de votre preuve du but suivant en sous-entendant les réécritures et
PreuveParties AuB dans B alpha
Donner les tactiques de votre preuve du but suivant en sous-entendant les réécritures et
PreuveParties AuB dans B alphainv
Donner les tactiques de votre preuve du but suivant en sous-entendant les réécritures et
PreuveParties AuB dans B grat
Donner les tactiques de votre preuve du but suivant en sous-entendant les réécritures et
PreuveParties A dans AnB alpha
Donner les premières tactiques de votre preuve du but suivant en sous-entendant les réécritures et
PreuveParties A dans AnB alphainv
Donner les tactiques de votre preuve du but suivant en sous-entendant les réécritures et
PreuveParties AuA dans BnB alpha
Donner les tactiques de votre preuve du but suivant en sous-entendant les réécritures et
PreuveParties A dans AnB alpha vrai
Donner les tactiques de votre preuve du but suivant en sous-entendant les réécritures et
PreuveParties Bob1
Bob est un boulet. Il a cru trouver une preuve de à savoir: Recopier la partie de sa preuve qui est correcte.
PreuveParties Bob1
Bob est un boulet. Il a cru trouver une preuve de à savoir: Recopier la partie de sa preuve qui est correcte.
PreuveParties régularité
Donner les tactiques de votre preuve du but suivant
Privilégier le contexte tacdiff
Privilégier le contexte test
XC Traduire un énoncé formel (entiers) V
2 Traduire (intervalles) V30
Recip1
Recip2
Recip3
Recip4
Somme de Cauchy inverse vrai
Voici un énoncé qu'on aurait pu trouver sur le web, suivi de sa preuve :
La somme de deux suites de Cauchy est de Cauchy. Preuve. Soient u et v deux suites de Cauchy. Nous savons qu'on a
et
.
On en déduit que, pour tout n et m
, on a
,
ce qui prouve que u+v est de Cauchy.
Ce texte vous inspire diverses preuves qui diffèrent par l'ordre des tactiques. Avec les blocs ci-dessous, formez le sous-enchaînement de 14 tactiques Forall et Exist dans l'une de ces variantes, en choisissant celle qui donne la réponse optimale pour l'ordre alphabétique INVERSE.
ZModele de mariages
Etablissez la correspondance entre les symboles et leurs sens ci-dess ous.
1 Evaluer (table de vérité) V20?
Ecrire la table de vérité de
XD Tac grat but 5 fini V17
Témoigner V20
Dans le contexte s'attaque au but Il propose la tactique ExistB avec pour témoin Pourra-t-il s'en tirer?
ZModele paup QCM
Quelle est la traduction de l'énoncé suivant:
?
ZModele QCM
Quelle est la nature fonctionnelle de "" dans la phrase suivante?
.
Typer complexes pap V5
Typer fonctions pap V8
Typer parties V1
Typer réelscompl V8
Typer réels V5
Typer entiers pap V2
Variables libres (énoncés) V30
Dans l'énoncé suivant, identifier les variables libres.
(ATTENTION: Séparez vos variables par des virgules. Tapez VIDE si la liste de variables répondant à la question est vide. Le comparateur distingue les majuscules des minuscules.)
Variables libres (formules) V30
Dans l'énoncé suivant, identifier les variables libres.
(ATTENTION: Séparez vos variables par des virgules. Tapez VIDE si la liste de variables répondant à la question est vide. Le comparateur distingue les majuscules des minuscules.)
Variables libres texte V1
Dans le début de phrase suivant, identifier les variables libres.
(ATTENTION: Séparez vos variables par des virgules. Tapez VIDE si la liste de variables répondant à la question est vide. Le comparateur distingue les majuscules des minuscules.)
XC Définir finit constante
Ici
est une fonction. En vous inspirant de f finit nulle ssi
définir:
XC Définir finit positive
Ici
est une fonction. En vous inspirant de f finit nulle ssi
définir:
1 Nier finit positive
Ici
est une fonction. Nier :
1 Nier finit constante
Ici
est une fonction. Nier :
XD Début gratuit
XD Début gratuit but/contexte
XD Formaliser intervalles
XD Tac SuiteEtFin V12
XD Tac grat but courant
On commence la preuve de l'énoncé : en appliquant autant que possible les sept tactiques gratuites ImpB EtC EtB OuB OuC ForallB ExistsC. Une fois que c'est fait, quel est le but courant?
XD tac grat nb var
On essaie de prouver l'énoncé : en appliquant autant que possible les six tactiques gratuites EtC EtB OuB OuC ForallB ExistsC. Une fois que c'est fait, combien le contexte courant contient-il de variables?
XE 5tactiques Entrainement
XE 5tactiques test
XE Preuves Fonctions diverses Entrainem
XE Preuves Fonctions diverses Test
XE Tac 8 fonctions Entrainement
XE Tac 8 fonctions Test
XE Tac Entrainement
XE Tac Test
ZZ1 NewTraduire f
(Choisissez -- si l'énoncé est toujours vrai.)
XG Newtactiques
XG NewDéfinir finit
Ici
est une fonction. En vous inspirant de f finit nulle ssi
définir:
XG Newevaluer (table de vérité) V10
Ecrire la table de vérité de
XG NewFormaliser mijo
XG NewFormaliser croissances
1 NewNier finit positive
Ici
est une fonction. Nier :
XG Tac 8 fonctions Entrainement
XG Tac A modifier 1
XG Tac A modifier 2
XG Tac A modifier 3
XG Tac Entrainement
XG Tac New8 fonctions Entrainement
XG Tac grat but 5 fini V17
XG NewTraduire f
(Choisissez -- si l'énoncé ne dit rien.)
XG NewTraduire
YEns Associativité de la réunion B
Donner une liste de tactiques qui commence la preuve de
[on agira d'abord et s'il reste du choix on privilégiera l'ordre des tactiques; Attention, OuB désigne le Ou faible (non gratuit)].
YEns Associativité de la réunion C
Donner une liste de tactiques qui commence la preuve de
[on agira d'abord et s'il reste du choix on privilégiera l'ordre des tactiques; Attention, OuB désigne le Ou faible (non gratuit)].
YEns Associativité de la réunion Alpha
Donner une liste de tactiques qui commence la preuve de
[On privilégiera l'ordre des tactiques; Attention, OuB désigne le Ou faible (non gratuit)].
YEns Associativité de la réunion Antialp
Donner une liste de tactiques qui commence la preuve de
[On privilégiera l'ordre des tactiques; Attention, OuB désigne le Ou faible (non gratuit)].
YEns NbTacAlpha Associativité de la réun
Vous avez commencé votre preuve de
par la liste de tactiques
.
Vous êtes donc confronté à un certain objectif courant et vous continuez cette preuve . Donner le nombre de tactiques qu'il vous faut exécuter pour venir à bout de cet objectif courant.
Les tactiques disponibles sont: ForallB, ForallC, ReecB, ReecC, ExistB, ExistC, EtB, EtC, ImpB, ImpC, OuB, OuC, Hyp [Attention, OuB désigne le Ou faible (non gratuit)].
YEns NbTacAlpha Associativité de l'inter
Vous avez commencé votre preuve de
par la liste de tactiques
.
Vous êtes donc confronté à un certain objectif courant et vous continuez cette preuve . Donner le nombre de tactiques qu'il vous faut exécuter pour venir à bout de cet objectif courant.
Les tactiques disponibles sont: ForallB, ForallC, ReecB, ReecC, ExistB, ExistC, EtB, EtC, ImpB, ImpC, OuB, OuC, Hyp [Attention, OuB désigne le Ou faible (non gratuit)].
YEns NbTacAlpha Croissance de l'intersec
Vous avez commencé votre preuve de
par la liste de tactiques
.
Vous êtes donc confronté à un certain objectif courant et vous continuez cette preuve . Donner le nombre de tactiques qu'il vous faut exécuter pour venir à bout de cet objectif courant.
Les tactiques disponibles sont: ForallB, ForallC, ReecB, ReecC, ExistB, ExistC, EtB, EtC, ImpB, ImpC, OuB, OuC, Hyp [Attention, OuB désigne le Ou faible (non gratuit)].
YF NbTacAlphaIdempotence inter
Vous avez commencé votre preuve de
par la liste de tactiques
.
Vous êtes donc confronté à un certain objectif courant et vous continuez cette preuve . Donner le nombre de tactiques qu'il vous faut exécuter pour venir à bout de cet objectif courant.
Les tactiques disponibles sont: ForallB, ForallC, ReecB, ReecC, ExistB, ExistC, EtB, EtC, ImpB, ImpC, OuB, OuC, Hyp, VraiB, FauxC [Attention, OuB désigne le Ou faible (non gratuit)].
YF NbTacAlphaIdempotence reu
Vous avez commencé votre preuve de
par la liste de tactiques
.
Vous êtes donc confronté à un certain objectif courant et vous continuez cette preuve . Donner le nombre de tactiques qu'il vous faut exécuter pour venir à bout de cet objectif courant.
Les tactiques disponibles sont: ForallB, ForallC, ReecB, ReecC, ExistB, ExistC, EtB, EtC, ImpB, ImpC, OuB, OuC, Hyp, VraiB, FauxC [Attention, OuB désigne le Ou faible (non gratuit)].
YF NbTacAlpha Neutralité du vide
Vous avez commencé votre preuve de
par la liste de tactiques
.
Vous êtes donc confronté à un certain objectif courant et vous continuez cette preuve . Donner le nombre de tactiques qu'il vous faut exécuter pour venir à bout de cet objectif courant.
Les tactiques disponibles sont: ForallB, ForallC, ReecB, ReecC, ExistB, ExistC, EtB, EtC, ImpB, ImpC, OuB, OuC, Hyp, VraiB, FauxC [Attention, OuB désigne le Ou faible (non gratuit)].
YF NbTacAlpha vide absorbant
Vous avez commencé votre preuve de
par la liste de tactiques
.
Vous êtes donc confronté à un certain objectif courant et vous continuez cette preuve . Donner le nombre de tactiques qu'il vous faut exécuter pour venir à bout de cet objectif courant.
Les tactiques disponibles sont: ForallB, ForallC, ReecB, ReecC, ExistB, ExistC, EtB, EtC, ImpB, ImpC, OuB, OuC, Hyp, VraiB, FauxC [Attention, OuB désigne le Ou faible (non gratuit)].
YG Associativité de la réunion
Donner les premières tactiques qu'il vous faut exécuter pour prouver
.
[Attention, OuB désigne le Ou faible (non gratuit)].
YG Commutativité de la réunion
Donner les 15 premières tactiques qu'il vous faut exécuter pour prouver
.
[Attention, OuB désigne le Ou faible (non gratuit)].
YG Commutativité de la réunion backup
Donner les 15 premières tactiques qu'il vous faut exécuter pour prouver
.
[Attention, OuB désigne le Ou faible (non gratuit)].
YH La réunion minore les majorants
Donner les tactiques qu'il vous faut exécuter pour prouver
.
[Attention, OuB désigne le Ou faible (non gratuit)].
YH L'intersection majore les minorants
Donner les tactiques qu'il vous faut exécuter pour prouver
.
[Attention, OuB désigne le Ou faible (non gratuit)].
YG Partie minimum
Donner les tactiques qu'il vous faut exécuter pour prouver
.
[Attention, OuB désigne le Ou faible (non gratuit)].
YG Reflexivité de l'inclusion
Donner les tactiques qu'il vous faut exécuter pour prouver
.
[Attention, OuB désigne le Ou faible (non gratuit)].
YG Transitivité de l'inclusion
Donner les tactiques qu'il vous faut exécuter pour prouver
.
[Attention, OuB désigne le Ou faible (non gratuit)].
YH L'intersection est commutative ter
Donner les tactiques qu'il vous faut exécuter pour prouver
.
YH L'intersection est commutative vrai
Donner les tactiques qu'il vous faut exécuter pour prouver
.
[Attention, OuB désigne le Ou faible (non gratuit)].
YH Monotonie complémentaire
Alice a commencé sa preuve de
par une liste de huit tactiques privilégiant l'action au but. Elle a ensuite fait une réécriture au contexte puis une contraposition.
Vous êtes donc confronté à un certain objectif courant et vous continuez cette preuve. Donner le nombre de tactiques qu'il vous faut exécuter pour venir à bout de cet objectif courant.
Les tactiques disponibles sont: ForallB, ForallC, ReecB, ReecC, ExistB, ExistC, EtB, EtC, ImpB, ImpC, OuB, OuC, Hyp [Attention, OuB désigne le Ou faible (non gratuit)].
YH Une invocation
Vous commencez votre preuve de
par ForallB ImpB EtC EtC puis vous invoquez le théorème qui dit que l'image d'une fonction continue est un intervalle. Donnez la liste des trois tactiques que vous exécutez ensuite pour exploiter cette ressource..
[Attention, OuB désigne le Ou faible (non gratuit)].
YH Utilisation d'une limite
Vous commencez votre preuve de
par ForallB ImpB EtC EtC ForallB. Après ça, vous invoquez le théorème des valeurs intermédiaires d'où vous déduisez que l'image de votre fonction est un intervalle. Vous réécrivez alors l'hypothèse concernant la limite en
. Donnez la liste des quatre tactiques que vous exécutez ensuite en vue d'exploiter cette hypothèse.
[Attention, OuB désigne le Ou faible (non gratuit)].
YH menage assoc inter
Alice propose à Bob une preuve de
conçue .
Mais Bob ne supporte pas les hypothèses ou les variables inutiles. Combien de tactiques proposées par Alice, Bob va-t-il accepter avant de faire du ménage?
Les tactiques utilisées par Alice sont: ForallB, ForallC, ReecB, ReecC, ExistB, ExistC, EtB, EtC, ImpB, ImpC, OuB, OuC, Hyp [Attention, OuB désigne le Ou faible (non gratuit)].
YH menage commut inter nombre
Alice propose à Bob une preuve de
conçue .
Mais Bob ne supporte pas les hypothèses ou les variables inutiles. Combien de fois Bob va-t-il interrompre la preuve d'Alice pour faire du ménage?
Les tactiques utilisées par Alice sont: ForallB, ForallC, ReecB, ReecC, ExistB, ExistC, EtB, EtC, ImpB, ImpC, OuB, OuC, Hyp [Attention, OuB désigne le Ou faible (non gratuit)].
YH menage commut inter rang
Alice propose à Bob une preuve de
conçue .
Mais Bob ne supporte pas les hypothèses ou les variables inutiles. Combien de tactiques d'Alice Bob va-t-il accepter avant de faire du ménage?
Les tactiques utilisées par Alice sont: ForallB, ForallC, ReecB, ReecC, ExistB, ExistC, EtB, EtC, ImpB, ImpC, OuB, OuC, Hyp [Attention, OuB désigne le Ou faible (non gratuit)].
YH menage monot inter
Alice propose à Bob une preuve de
conçue .
Mais Bob ne supporte pas les hypothèses ou les variables inutiles. Combien de tactiques proposées par Alice Bob va-t-il accepter avant de faire du ménage?
Les tactiques utilisées par Alice sont: ForallB, ForallC, ReecB, ReecC, ExistB, ExistC, EtB, EtC, ImpB, ImpC, OuB, OuC, Hyp [Attention, OuB désigne le Ou faible (non gratuit)].
YK Composition d' injectives
Bob prouve
,
. Il exécute 16 tactiques et envisage de poursuivre avec ImpC. Mais Alice lui fait observer que, s'il veut s'en sortir, il doit d'abord faire autre chose. A quelle tactique pense-t-elle?
YK Composition de surjectives, nb de tac
Bob prouve
,
. Il exécute 11 tactiques et envisage de poursuivre avec ExistB. Mais Alice lui fait observer que, s'il veut s'en sortir, il doit d'abord faire autre chose. Combien de tactiques préconise-t-elle d'exécuter avant ExistB?
YK Composition de surjectives, coups de
Bob prouve
,
Il choisit la stratégie qui lui permet d'exécuter ExistB au plus vite. Sachant qu'il est pressé, combien de tactiques va-t-il exécuter après ExistB pour conclure?
YK Composition injective
Alice prouve
,
. Elle exécute 12 tactiques et envisage de poursuivre avec ImpC. Mais Bob lui fait observer que, si elle veut s'en sortir, elle doit d'abord faire autre chose. A quelle tactique pense-t-il?
YK Composition injective, but courant
Alice prouve
.
Elle exécute 12 tactiques et poursuit avec ImpB et ImpC. Ensuite elle effectue deux réécritures au but, et invoque Refl. Combien de tactiques lui faut-il pour venir à bout de son but courant?
YK Composition injective, coups de grâce
Alice prouve
.
Elle exécute 12 tactiques et poursuit avec ImpB et ImpC. Ensuite elle effectue deux réécritures au but, et invoque Refl. Combien de tactiques lui faut-il pour finir sa preuve?
YK Composition surjective, nb de tac
Bob prouve
.
. Il a exécuté 9 tactiques et envisage de poursuivre avec ExistB. Mais Alice lui fait observer que, s'il veut s'en sortir, il doit d'abord faire autre chose. Combien de tactiques préconise-t-elle d'exécuter maintenant avant ExistB?
YK Injections monos, but courant
Alice prouve
.
Elle exécute 15 tactiques et poursuit avec ImpC. Ensuite elle effectue deux réécritures au contexte. Combien de tactiques lui faut-il alors pour venir à bout de son but courant?
YK Injections monos, coups de grâce
Alice prouve
.
Elle exécute 16 tactiques . Ensuite elle effectue deux réécritures au contexte. Combien de tactiques lui faut-il alors pour venir à bout de sa preuve?
YK Surjections épis, nb de tac
Alice prouve
.
Combien de tactiques doit-elle exécuter avant de faire son deuxième ForallC?
YK Surjections épis, coups de grâce
Alice prouve
.
Elle a fait ses deux ForallC au plus vite. Elle fait ensuite les réécritures utiles. Combien de tactiques doit-elle exécuter après ces réécritures pour finir sa preuve?
ZX11 NewTraduire f
(Choisissez -- si l'énoncé est toujours vrai.)
ZX13 NewTraduire f
(Choisissez -- si l'énoncé est toujours vrai.)
ZX14 NewTraduire f
(Choisissez -- si l'énoncé est toujours vrai.)
ZZ11 NewTraduire f
(Choisissez -- si l'énoncé est toujours vrai.)
ZZ12 NewTraduire f
(Choisissez -- si l'énoncé est toujours vrai.)
ZZ13 NewTraduire f
(Choisissez -- si l'énoncé est toujours vrai.)
ZZ14 NewTraduire f
(Choisissez -- si l'énoncé est toujours vrai.)
ZZ1 Définition et négation (Xiao)
Soit
une fonction réelle.
Formalisez la propriété ``
est ''. (Tirez les éléments pour composer votre formule)
La propriété ``
est '' se formalise en .
Quel est le contraire (négation) de cette propriété ?
Maintenant formalisez la négation ``
n'est pas ''.
La négation ``
n'est pas '' se formalise donc en . Donnez deux valeurs
,
pour montrer que la fonction ci-contre n'est pas , selon la formule. (Chaque case de la grille vaut 1 ; il faut donc choisir
et
entre -5 et 5.)
ZZ2' NewTraduire interv
ZZ2 Traduire (intervalles) V30
ZZ3 Définir finit positive
Ici
est une fonction. En vous inspirant de f finit nulle ssi
définir:
f commence négative
1 Nier finit positive
Ici
est une fonction. Nier : f commence négative
ZZ5 Formaliser intervalles
ZZ6
Donner une liste de six tactiques gratuites qui s'applique au but suivant [on sautera les explicitations. Au choix, on agira d'abord au contexte; et s'il reste du choix on privilégiera l'ordre alphabétique des tactiques]
Si une fonction finit affine ses multiples aussi.
ZZ7 New5tactiques
ZZ8 Tac New8 fonctions Entrainement
ZZ91 vide absorbant
Donner les tactiques qu'il vous faut exécuter pour prouver
.
[Attention, OuB désigne le Ou faible (non gratuit)].
ZZ92 ImRecInter0
ZZ92 ImRecInter1
ZZ92 ImRecInter2
ZZ92 ImRecInter3
ZZ92 ImRecInterDer
Voici maintenant l'énoncé suivi de sa preuve complète:
Preuve.
Avec les blocs proposés ci-dessous, formez la liste de 12 tactiques suggérée par le dernier alinéa de cette preuve.
ZZ92 ImRecInter0 vrai
ZZ92 ImRecInter1 vrai
ZZ9
Donner les 23 tactiques de votre preuve du but suivant en retardant au maximum les réécritures et en privilégiant les autres actions au but
ZSteps générique
Somme de Cauchy chaos
Voici un énoncé qu'on aurait pu trouver sur le web, suivi de sa preuve :
La somme de deux suites de Cauchy est de Cauchy. Preuve. Soient u et v deux suites de Cauchy. Nous savons qu'on a
et
.
On en déduit que, pour tout n et m
, on a
,
ce qui prouve que u+v est de Cauchy.
Ce texte vous inspire diverses preuves qui diffèrent par l'ordre des tactiques. Avec les blocs ci-dessous, formez le sous-enchaînement de 14 tactiques Forall et Exist dans l'une de ces variantes, en choisissant celle qui donne la réponse optimale pour l'ordre privilégiant ExistC devant ForallC, devant ForallB, devant ExistB. ATTENTION: les tactiques ne sont pas proposées dans cet ordre!!!!!!
ATTENTION: les tactiques ne sont pas proposées dans cet ordre!!!!!!
ATTENTION: les tactiques ne sont pas proposées dans cet ordre!!!!!!
ATTENTION: les tactiques ne sont pas proposées dans cet ordre!!!!!!
Somme de Cauchy direct
Voici un énoncé qu'on aurait pu trouver sur le web, suivi de sa preuve :
La somme de deux suites de Cauchy est de Cauchy. Preuve. Soient u et v deux suites de Cauchy. Nous savons qu'on a
et
.
On en déduit que, pour tout n et m
, on a
,
ce qui prouve que u+v est de Cauchy.
Cette preuve vous inspire un enchainement de tactiques. Avec les blocs ci-dessous, formez le sous-enchaînement correspondant de 14 tactiques Forall et Exist. On respectera l'ordre suggéré par la preuve et, au choix, on privilégiera l'ordre alphabétique.
convergence vers Cauchy au but
Voici un énoncé trouvé sur le web (www.math.univ-toulouse.fr/~yak/Suites-Poly.pdf , p.45), suivi de sa preuve :
Toute suite convergente est de Cauchy. Preuve. Soit u une suite convergente et soit
sa limite. Nous savons que
. On en déduit que, pour tout n et m
,
. ce qui prouve que u est de Cauchy.
Cette preuve vous inspire un enchainement de tactiques. Modifiez cet enchainement de façon a privilégier l'action au but. Puis, avec les blocs ci-dessous, formez le sous-enchaînement correspondant de tactiques Forall et Exist.
convergence vers Cauchy antialpha
Voici un énoncé trouvé sur le web (www.math.univ-toulouse.fr/~yak/Suites-Poly.pdf , p.45), suivi de sa preuve :
Toute suite convergente est de Cauchy. Preuve. Soit u une suite convergente et soit
sa limite. Nous savons que
. On en déduit que, pour tout n et m
,
. ce qui prouve que u est de Cauchy.
Vous devez concevoir un enchainement de tactiques prouvant cet énoncé, et donner le sous-enchaînement correspondant de tactiques Forall et Exist. Vous devez choisir une preuve conduisant à la réponse optimale du point de vue de l'ordre alphabétique inverse.
convergence vers Cauchy direct vrai
Voici un énoncé trouvé sur le web (www.math.univ-toulouse.fr/~yak/Suites-Poly.pdf , p.45), suivi de sa preuve :
Toute suite convergente est de Cauchy. Preuve. Soit u une suite convergente et soit
sa limite. Nous savons que
. On en déduit que, pour tout n et m
,
. ce qui prouve que u est de Cauchy.
Cette preuve vous inspire un enchainement de tactiques. Avec les blocs ci-dessous, formez le sous-enchaînement correspondant de tactiques Forall et Exist. On respectera l'ordre suggéré par la preuve et, dans le doute, on privilégiera l'ordre alphabétique.
convergence vers Cauchy inverse vrai
Voici un énoncé trouvé sur le web (www.math.univ-toulouse.fr/~yak/Suites-Poly.pdf , p.45), suivi de sa preuve :
Toute suite convergente est de Cauchy. Preuve. Soit u une suite convergente et soit
sa limite. Nous savons que
. On en déduit que, pour tout n et m
,
. ce qui prouve que u est de Cauchy.
Cette preuve vous inspire un enchainement de tactiques. Avec les blocs ci-dessous, formez le sous-enchaînement correspondant de tactiques Forall et Exist. On respectera l'ordre suggéré par la preuve et, dans le doute, on privilégiera l'ordre alphabétique inverse.
convergence vers Cauchy au but vrai
Voici un énoncé trouvé sur le web (www.math.univ-toulouse.fr/~yak/Suites-Poly.pdf , p.45), suivi de sa preuve :
Toute suite convergente est de Cauchy. Preuve. Soit u une suite convergente et soit
sa limite. Nous savons que
. On en déduit que, pour tout n et m
,
. ce qui prouve que u est de Cauchy.
Cette preuve vous inspire un enchainement de tactiques. Modifiez cet enchainement de façon a privilégier l'action au but. Puis, avec les blocs ci-dessous, formez le sous-enchaînement correspondant de tactiques Forall et Exist.
Cette page n'est pas dans son apparence habituelle parce que
WIMS n'a pas pu reconnaître votre navigateur web.
Veuillez noter que les pages WIMS sont générées interactivement; elles ne
sont pas des fichiers
HTML ordinaires. Elles doivent être utilisées interactivement EN LIGNE.
Il est inutile pour vous de les ramasser par un programme robot.
- Description: paquet d'exercices de Maths Discrètes pour la première année de Licence de Maths. This is the main site of WIMS (WWW Interactive Multipurpose Server): interactive exercises, online calculators and plotters, mathematical recreation and games
- Keywords: wims, mathematics, mathematical, math, maths, interactive mathematics, interactive math, interactive maths, mathematic, online, calculator, graphing, exercise, exercice, puzzle, calculus, K-12, algebra, mathématique, interactive, interactive mathematics, interactive mathematical, interactive math, interactive maths, mathematical education, enseignement mathématique, mathematics teaching, teaching mathematics, algebra, geometry, calculus, function, curve, surface, graphing, virtual class, virtual classes, virtual classroom, virtual classrooms, interactive documents, interactive document, Logique, preuve, formaliser, nier, tactique, traduire, énoncé, vrai, faux, quantificateur