Annuler
connectez vous
logique en post-bac
- Description de mathématique formelle-termes et relations
- Théorèmes
- Théories logiques
- Équations différentielles : un Cours complet avec des exemples
- Généralités sur les matrices, applications linéaires, changement de base, rang d'une matrice - supérieur
- Ensemble et application Partie II
- Un best-of d'exos de probabilités (après le bac)
- Espaces vectoriels et Applications linéaires - supérieur
Inscription / Connexion Nouveau Sujet
Accueil l'île des mathématiques Forum de mathématiquesListe de tous les forums de mathématiques SupérieurOn parle exclusivement de maths, pour le supérieur principalement, les BTS, IUT, prépas... Licence Maths 1e ann LogiqueTopics traitant de logique [tout]Lister tous les topics de mathématiques
Niveau Licence Maths 1e ann
Formalisation de la notion d'application
Posté par SkyMtn
Bonjour. La formalisation des objets mathématiques m'obsède (j'aimerai vraiment que ça cesse ^^), et du coup je me suis posé une question... comment s'assurer que lorsque l'on écrit par exemple , cela définit bien une application de
dans
(au sens des graphes dans ZFC) ?
Hormis refaire la démonstration que c'est une application en définissant en compréhension "l'ensemble des couples qui marchent"... c'est long, sans aucun intérêt, mais intuitivement on voit que c'est une application, mais la "formule" explicitant l'image n'a pas l'air d'être une formule de ZFC (car c'est pas une formule logique) pourtant on peut la "définir". Cela me perturbe un peu beaucoup 
Il n'y a pas un moyen de généraliser sans rentrer dans des histoires de "méta fonctions" ou je ne sais quoi ?
Je sais que ça a l'air stupide, mais j'ai l'impression qu'en maths il y a trop d'implicite :'(
Merci par avance pour vos réponses.
Bonjour.
Alors je sais qu'il y a plusieurs définitions possibles d'une application. Pour moi une application c'est essentiellement une partie d'ensembles.
Si , personnellement je comprends
Pour vérifier qu'il s'agit bien d'une application, il suffit de vérifier que l'assertion suivante est vraie :
soit
ce qui me paraît quand même assez vrai
Oui, c'est la définition usuelle d'application. Mais c'est inutile de devoir montrer ça à chaque fois quand on définit "explicitement" une application. La formule qui donne l'image est particulière, on peut pas la définir formellement
On pourrait imaginer que est un raccourci pour signifier que
, mais il reste à savoir ce qu'est exactement
? Une formule, laquelle (ou plutôt de quel "type") ?
SkyMtn @ 04-01-2018 à 14:30
Oui, c'est la définition usuelle d'application. Mais c'est inutile de devoir montrer ça à chaque fois quand on définit "explicitement" une application.
Oui, c'est la définition usuelle d'application. Mais c'est inutile de devoir montrer ça à chaque fois quand on définit "explicitement" une application.
Si inutile que ça ? Personnellement, lorsque je définis une application, je fais toujours attention à deux choses :
1) Tout élément de l'espace de départ a-t-il bien au moins une image dans l'espace d'arrivée ?
2) Tout élément de l'espace de départ a-t-il bien au plus une image dans l'espace d'arrivée ?
Finalement, c'est exactement revenir à la définition d'une application, à savoir
Je ne vois pas ce qu'il y a d'inutile à revenir à ça. D'ailleurs, c'est même essentiel lorsqu'il n'est pas clair que l'application est bien définie, typiquement par exemple lorsque l'espace d'arrivée est un ensemble quotient, et que l'on veut vérifier que l'image ne dépend pas du représentant choisi de la classe d'équivalence.
En fait je me complique la vie pour rien je crois 
Si on suppose que pour tout , il existe un élément
(l'indice ne sert qu'à marquer l'éventuelle dépendance de cette lettre par rapport à x, comme pour l'exemple de la fonction carrée), alors il existe une unique application f de X vers Y de sorte que pour tout
, on ait
(l'existence est assurée par l'hypothèse de départ qui permet de dire que tout objet de X est associé à au moins un élément de Y, l'unicité par construction en compréhension).
Citation :
La formalisation des objets mathématiques m'obsède (j'aimerai vraiment que ça cesse ^^)
La formalisation des objets mathématiques m'obsède (j'aimerai vraiment que ça cesse ^^)
J'ai eu aussi ma période, et ça m'a passé car c'est vraiment gonflant à force
; on arrête de faire des maths et on devient un employé de la sécu à force de formaliser. 
SkyMtn @ 04-01-2018 à 15:54
En fait je me complique la vie pour rien je crois
Si on suppose que pour tout
, il existe un élément 
(l'indice ne sert qu'à marquer l'éventuelle dépendance de cette lettre par rapport à x, comme pour l'exemple de la fonction carrée), alors il existe une unique application f de X vers Y de sorte que pour tout , on ait  = \phi_x)
(l'existence est assurée par l'hypothèse de départ qui permet de dire que tout objet de X est associé à au moins un élément de Y, l'unicité par construction en compréhension).
En fait je me complique la vie pour rien je crois
Si on suppose que pour tout
Pour le coup, l'existence n'a rien d'évidente puisqu'il s'agit là d'une des formulations de l'axiome du choix.
Mais l'axiome du choix est accepté dans ZFC donc il n'y a aucun soucis (il faut juste penser à le mentionner).
Mais si tu veux être tâtillon au point de te demander pourquoi la fonction carré est bien définie, je trouve qu'il est approprié de mentionner AC dès qu'on le voit, et surtout s'en passer dès qu'on le peut. Point de vue entièrement personnel.
Je préfère avec AC. A partir du moment où on a deux ensembles non vide, il existe une fonction de l'un dans l'autre. Pour x fixé dans X, on considère , comme le cartésien est non vide, d'après l'axiome du choix il existe
telle que pour tout
, par conséquent
et il existe alors un unique
tel que
. Il suffit de considérer f comme l'ensemble des ces couples là, non ?