Processing math: 100%

Ensembles et fonctions

Dans ce cours, on s'attarde un peu sur les notions d'ensembles et de fonctions, même ces notions intervenaient déjà implicitement dans certains exercices des cours précédents. Dans notre contexte, ces notions offrent surtout des exemples d'utilisations des connecteurs logiques et quantificateurs précédemment introduits.

Ensembles

En mathématique, un ensemble désigne une collection non-ordonnée d'objets distincts. La notation xA signifie que l'objet x fait partie de l'ensemble A. Pris dans son sens le plus large, ce mot « ensemble » n'impose aucune homogénéité de la collection, on peut considérer par exemple un ensemble {n,f,A} formé d'un entier n, d'une fonction f et d'un ensemble A de nombres réels. Outre le caractère un peu artificiel de ces ensembles hétérogènes, leur utilisation nécessite des axiomes très précautionneux pour interdire la formation d'ensembles conduisant à des contradictions logiques. Ainsi il est indispensable que les axiomes de la théorie des ensembles interdisent de considérer l'ensemble des ensembles qui ne se sont pas éléments d'eux-mêmes. En effet, si un tel ensemble R existait, on devrait avoir soit RR, mais alors RR par définition de R, soit RR, ce qui entraînerait RR par définition de R (c'est le paradoxe de Russel).

Ces considérations subtiles sur les règles de formation d'ensembles valides ne font pas du tout partie des objectifs visés par ce cours. Nous travaillerons toujours avec des ensembles formés d'objets mathématiques ayant un type X fixé à l'avance. Par exemple des ensembles de nombres entiers, ou de nombres réels, ou bien des ensembles de fonctions réelles d'une variable réelle etc. La donnée d'un tel ensemble est équivalente à la donné d'un prédicat sur X. En effet, tout ensemble A d'objet de type X donne naissance au prédicat P défini par : Px si et seulement si xA. Autrement dit, pour tout x, P associe à x l'énoncé xA. Réciproquement, si P est un prédicat sur X, on peut former l'ensemble des x pour lesquels Px est vrai, on le note {x|Px}. Par exemple, l'ensemble des entiers naturels pairs est {n|k,n=2k}. Il est important de noter que la variable x est liée dans la notation {x|Px}. Elle ne peut pas s'échapper de la formule pour se référer au contexte, et elle peut être renommée.

Dans le cas des ensemble finis, on peut aussi décrire un ensemble en énumérant ses éléments. Le prédicat associé est une disjonction d'égalités. Par exemple, on peut considérer l'ensemble d'entiers naturels {0,42}, qui correspond au prédicat qui associe à n l'énoncé « n=0 ou n=42 ».

Les ensembles vérifient le principe d'extensionnalité : deux ensembles A et B sont égaux si et seulement si x,xAxB. Autrement dit, deux ensembles sont égaux si les prédicats associés fournissent des énoncé universellement équivalents.

Enfin on remarque que chaque ensemble A d'objets de type X donne lieu à des abréviations de quantification bornée. Si P est un prédicat sur X, la formule xA,Px est l'abréviation de x,xAPx. De même la formule xA,Px est l'abréviation de x,xA et Px.

Dans Lean, on note set X le type des ensembles d'objets de type X. Si P : X → Prop est un prédicat sur X, l'ensemble associé est noté {x | P x}, ou bien {x : X | P x} si on souhaite expliciter X. Cette notation est purement décorative, Lean ne fait essentiellement aucune distinction entre P et {x | P x}. De même, la notation a ∈ {x | P x} est simplement une façon d'écrire P a. On peut forcer Lean à passer de l'un à l'autre en utilisant rw set.mem_set_of_eq mais il s'agit d'une opération essentiellement esthétique.

On peut aussi utiliser la notation {0, 42} comme ci-dessus mais à condition que le type des éléments soit clair d'après le contexte, ou bien en spécifiant ({0, 42} : set ℕ).

Lorsque le but est de démontrer une égalité d'ensembles A = B, la commande ext x invoque le principe d'extensionnalité en nommant x la variable et en l'introduisant dans le contexte, transformant ainsi le but en x ∈ A ↔ x ∈ B.

Exemple

Montrons que l'entier 8 fait partie de l'ensemble des entiers pairs.

example : 8  { n |  k, n = 2*k} :=
Démonstration
Il s'agit de montrer qu'il existe k tel que 8=2k.Or k=4 fait l'affaire,
  use 4,
 8  {n :  |  (k : ), n = 2 * k}
 8 = 2 * 4
c'est un calcul direct.
  ring,
 8 = 2 * 4
no goals
QED.
 8  {n :  |  (k : ), n = 2 * k}

Inclusion d'ensembles

Après l'égalité, la relation la plus importante entre ensembles est celle d'inclusion. On dit que A est inclus dans B si tout élément de A est aussi élément de B : x,xAxB. On note cela AB ou AB. Le premier symbole est parfois réservé aux inclusions strictes, c'est à dire au cas où A est inclus dans B mais n'est pas égal à B. Cependant il s'agit d'une convention assez rare, le symbole usuel pour l'inclusion stricte étant plutôt AB.

Si A et B correspondent aux prédicats P et Q respectivement, on peut réécrire AB comme x,PxQx. On remarque ici qu'il est crucial que l'énoncé PxQx soit vrai lorsque Px est faux : l'énoncé AB n'affirme rien concernant les éléments qui ne sont pas dans A.

Pour démontrer (directement) AB, on commence donc par écrire « Soit x un élément de A ».

Dans Lean, la notation utilisée pour l'inclusion est , ce qui évite toute ambiguïté. Si A = {x | P x} et B = {x | Q x}, la notation A ⊆ B est purement décorative, Lean ne fait aucune différence entre cette notation et ∀ x, P x → Q x. En particulier on commencera la démonstration de A ⊆ B par intros x hxA pour introduire un objet x et une hypothèse hxA : x ∈ A.

Exemple

Montrons que {n|k,n=8k}{n|k,n=4k}. On prêtera une attention particulière au fait que les deux k apparaissant dans cette formule sont liés indépendamment, il n'y a donc aucune raison qu'ils désignent le même entier.

example : {n |  k, n = 8*k}  {n |  k, n = 4*k} :=
Démonstration
Soit n dans {n|k,n=8k}
  intros n hn,
 {n :  |  (k : ), n = 8 * k}  {n :  |  (k : ), n = 4 * k}
n : ,
hn : n  {n :  |  (k : ), n = 8 * k}
 n  {n :  |  (k : ), n = 4 * k}
l'hypothèse sur n fournit k tel que n=8k.
  cases hn with k hk,
n : ,
hn : n  {n :  |  (k : ), n = 8 * k}
 n  {n :  |  (k : ), n = 4 * k}
n k : ,
hk : n = 8 * k
 n  {n :  |  (k : ), n = 4 * k}
Montrons que l=2k convient pour écrire n=4l.
  use 2*k,
n k : ,
hk : n = 8 * k
 n  {n :  |  (k : ), n = 4 * k}
n k : ,
hk : n = 8 * k
 n = 4 * (2 * k)
Il suffit d'utiliser que n=8k et de calculer.
  rw hk,
n k : ,
hk : n = 8 * k
 n = 4 * (2 * k)
n k : ,
hk : n = 8 * k
 8 * k = 4 * (2 * k)
  ring,
n k : ,
hk : n = 8 * k
 8 * k = 4 * (2 * k)
no goals
QED.
 {n :  |  (k : ), n = 8 * k}  {n :  |  (k : ), n = 4 * k}

Le principe d'extensionnalité montre que, pour démontrer une égalité d'ensembles A=B, il suffit de montrer AB et BA. Cela correspond simplement au fait qu'une équivalence est la conjonction de deux implications. Une telle démonstration est souvent appelée « démonstration par double inclusion ».

Dans Lean, on peut commencer par utiliser la commande d'extensionnalité ext x puis split pour scinder l'équivalence en deux implications comme d'habitude, ou bien utiliser apply set.subset.antisymm pour obtenir deux inclusions à démontrer.

Intersection et réunion

Soit A et B deux ensembles. L'intersection de A et B est l'ensemble des objets qui sont dans A et dans B. On le note AB. Si A et B correspondent aux prédicats P et Q respectivement alors le prédicat correspondant à AB associe à x l'énoncé « Px et Qx ». Pour démontrer que x est dans AB, il faut donc démontrer que x est dans A et démontrer que x est dans B. Lorsqu'une hypothèse affirme que x est dans AB, on peut utiliser que x et dans A et utiliser que x est dans B.

Lean utilise la notation A ∩ B, mais ne fait aucune différence entre A ∩ B et {x | x ∈ A ∧ x ∈ B}. Ainsi, pour montrer x ∈ A ∩ B, on peut utiliser split puis donner une démonstration de x ∈ A suivie d'une démonstration de x ∈ B.

Exemple

Montrons que ABB

example (X : Type) (A B : set X) : A  B  B :=
Démonstration
Soit x un élément de AB.
  intros x hyp,
X : Type,
A B : set X
 A  B  B
X : Type,
A B : set X,
x : X,
hyp : x  A  B
 x  B
Par hypothèse, x est dans A et x est dans B.
  cases hyp with hxA hxB,
X : Type,
A B : set X,
x : X,
hyp : x  A  B
 x  B
X : Type,
A B : set X,
x : X,
hxA : x  A,
hxB : x  B
 x  B
En particulier x est dans B
  exact hxB,
X : Type,
A B : set X,
x : X,
hxA : x  A,
hxB : x  B
 x  B
no goals
QED.
X : Type,
A B : set X
 A  B  B

La réunion de A et B est l'ensemble des objets qui sont soit dans A soit dans B. On le note AB. Si A et B correspondent aux prédicats P et Q respectivement alors le prédicat correspondant à AB associe à x l'énoncé « Px ou Qx ». Pour démontrer (directement) que x est dans AB, il faut donc démontrer que x est dans A ou bien démontrer que x est dans B. Lorsqu'une hypothèse affirme que x est dans AB, son utilisation déclenche un embranchement dans la démonstration, avec une branche dans laquelle on suppose que x est dans A et une branche dans laquelle on suppose que x est dans B.

Lean utilise la notation A ∪ B, mais ne fait aucune différence entre A ∪ B et {x | x ∈ A ∨ x ∈ B}. Ainsi, pour montrer x ∈ A ∪ B, on peut utiliser left puis donner une démonstration de x ∈ A ou bien utiliser right puis donner une démonstration de x ∈ B.

Exemple

Montrons que AAB

example (X : Type) (A B : set X) : A  A  B :=
Démonstration
Soit x un élément de A
  intros x hxA,
X : Type,
A B : set X
 A  A  B
X : Type,
A B : set X,
x : X,
hxA : x  A
 x  A  B
Pour montrer que x est dans AB, il suffit de montrer qu'il est dans A
  left,
X : Type,
A B : set X,
x : X,
hxA : x  A
 x  A  B
X : Type,
A B : set X,
x : X,
hxA : x  A
 x  A
C'est ce que nous avons supposé.
  exact hxA,
X : Type,
A B : set X,
x : X,
hxA : x  A
 x  A
no goals
QED.
X : Type,
A B : set X
 A  A  B

Il existe une troisième opération de base, le passage au complémentaire, mais elle ne sera abordée que dans le chapitre suivant, qui concerne la négation d'énoncés.

Fonctions

Une fonction entre deux ensembles X et Y un objet f qui associe à tout élément x de X un unique objet de Y, noté f(x). On dit que X est la source de f (ou son ensemble de départ) et Y son but (ou ensemble d'arrivée). On dit aussi que f est une fonction « de X dans Y ». Les exemples les plus simples sont les fonctions constantes, qui envoient tous les éléments de X sur un même élément de Y, et, pour chaque ensemble X, la fonction « identité de X », notée IdX, qui envoie tout élément x sur lui-même.

La notion de fonction est extrêmement générale. Elle s'applique bien sûr aux fonctions réelles d'une variable réelle (X=Y=) mais aussi aux suites de nombres réels (X=, Y=) et à bien d'autres situations (nous en croiserons quelques autres plus bas). Les fonctions les plus faciles à appréhender sont définies par une expression où apparaît explicitement un élément x de l'ensemble de départ X. Ainsi on peut considérer la fonction f de dans définie par f(x)=x2. Pour parler de cette fonction sans la nommer, les mathématiciens utilisent le plus souvent la notation xx2, qui se lit « x va sur x2 » ou « la fonction qui envoie x sur x2 ». Cette notation est très concise mais cache un peu le fait que la variable est liée par le symbole . Les informaticiens préfèrent utiliser la notation λx,x2, qui rappelle plus directement les notations utilisées pour les quantificateurs. Cette notation est utilisée par Lean mais aussi par python par exemple, sous la forme lambda x: x**2 en python.

Cependant ces fonctions définies explicitement par une expression sont loin d'épuiser toutes les façons de définir des fonctions. Dans le cas d'une suite, c'est à dire d'une fonction de dans , on peut par exemple utiliser une définition par récurrence. Ainsi la phrase « soit u la suite définie par u0=1 et un+1=sin(un) » définit sans ambiguïté une suite de nombre réels mais on ne peut pas donner d'expression de un en fonction de n. La définition « soit exp l'unique solution de l'équation différentielle y=y qui vaut un en zéro » est aussi une définition de fonction parfaitement légitime une fois démontré l'existence et l'unicité d'une telle solution, bien que cette démonstration ne fournisse pas d'expression pour les solutions. Une autre façon très courante de produire de nouvelles fonctions est l'opération de composition. Si X, Y et Z sont des ensembles et f:XY et g:YZ des fonctions alors la fonction gf est, par définition, la fonction de X dans Z qui envoie x sur g(f(x)).

Les fonctions de X dans Y forment elles aussi un type d'objets mathématiques à part entière, on le note YX ou XY, et il peut apparaître comme source ou but d'autres fonctions. Par exemple, on peut considérer la fonction de dans définie par x(yxy). À tout nombre réel x, cette fonction associe la fonction qui à tout nombre réel y associe le nombre produit xy. Les ensembles de fonctions peuvent aussi apparaître comme sources de fonctions. Ainsi l'opération de dérivation d'une fonction est une fonction de {f:|f est derivable} dans .

L'analogue du principe d'extensionnalité des ensemble est le principe d'extensionnalité pour les fonctions, qui stipule que deux fonctions f et g, ayant même source et même but, sont égales si et seulement si elles prennent la même valeur partout : f=gx,f(x)=g(x).

On dit qu'un fonction f de X dans Y est injective si xxX,f(x)=f(x)x=x. On dit qu'elle est surjective si yY,xX,f(x)=y. On dit qu'elle est bijective si elle est injective et surjective. La bijectivité de f est équivalente à l'existence d'une fonction g de Y dans X telle que gf=IdX et fg=IdY. La fonction g est alors unique, elle est appelée réciproque de f.

Dans Lean, le type des fonctions de X dans Y est noté X → Y. L'égalité (g ∘ f) x = g (f x) ne nécessite aucune démonstration, c'est la définition de g ∘ f. Cependant on peut forcer le passage d'une écriture à l'autre en utilisant rw function.comp_app (ou rw ← function.comp_app dans l'autre sens). Pour montrer une égalité de fonction f = g en utilisant le principe d'extensionnalité, on utilise la commande ext x qui introduit une variable x dans la source commune à f et g et transforme le but en f x = g x.

Exemple

Montrons que si gf est injective alors f est injective.

example (X Y Z : Type) (f : X  Y) (g : Y  Z) :
( x x', (g  f) x = (g  f) x'  x = x')  ( x x', f x = f x'  x = x') :=
Démonstration
Supposons que g ∘ f est injective.
  intro hyp,
X Y Z : Type,
f : X  Y,
g : Y  Z
 ( (x x' : X), (g  f) x = (g  f) x'  x = x')   (x x' : X), f x = f x'  x = x'
X Y Z : Type,
f : X  Y,
g : Y  Z,
hyp :  (x x' : X), (g  f) x = (g  f) x'  x = x'
  (x x' : X), f x = f x'  x = x'
Soit x et x dans X tels que f(x)=f(x).On doit montrer que x=x.
  intros x x' hxx',
X Y Z : Type,
f : X  Y,
g : Y  Z,
hyp :  (x x' : X), (g  f) x = (g  f) x'  x = x'
  (x x' : X), f x = f x'  x = x'
X Y Z : Type,
f : X  Y,
g : Y  Z,
hyp :  (x x' : X), (g  f) x = (g  f) x'  x = x',
x x' : X,
hxx' : f x = f x'
 x = x'
Comme gf est injective, il suffit de montrer que(gf)(x)=(gf)(x),
  apply hyp,
X Y Z : Type,
f : X  Y,
g : Y  Z,
hyp :  (x x' : X), (g  f) x = (g  f) x'  x = x',
x x' : X,
hxx' : f x = f x'
 x = x'
X Y Z : Type,
f : X  Y,
g : Y  Z,
hyp :  (x x' : X), (g  f) x = (g  f) x'  x = x',
x x' : X,
hxx' : f x = f x'
 (g  f) x = (g  f) x'
c'est à dire g(f(x))=g(f(x)),
  rw function.comp_app,
X Y Z : Type,
f : X  Y,
g : Y  Z,
hyp :  (x x' : X), (g  f) x = (g  f) x'  x = x',
x x' : X,
hxx' : f x = f x'
 (g  f) x = (g  f) x'
X Y Z : Type,
f : X  Y,
g : Y  Z,
hyp :  (x x' : X), (g  f) x = (g  f) x'  x = x',
x x' : X,
hxx' : f x = f x'
 g (f x) = (g  f) x'
qui découle de l'hypothèse f(x)=f(x).
  rw hxx',
X Y Z : Type,
f : X  Y,
g : Y  Z,
hyp :  (x x' : X), (g  f) x = (g  f) x'  x = x',
x x' : X,
hxx' : f x = f x'
 g (f x) = (g  f) x'
no goals
QED.
X Y Z : Type,
f : X  Y,
g : Y  Z
 ( (x x' : X), (g  f) x = (g  f) x'  x = x')   (x x' : X), f x = f x'  x = x'

Image directe et image inverse

Par définition, une fonction f de X dans Y transporte les éléments de X vers Y. Mais on peut aussi transporter ces éléments par paquets. Si A est une partie de X, l'image de A par f est définie comme l'ensemble des valeurs prises par f sur les éléments de A, c'est à dire {y|xA,f(x)=y}. On la note f(A), bien que cette notation soit assez dangereuse puisqu'elle pourrait laisser croire que A est un élément de X. Ainsi, pour démontrer yf(A), il faut fournir x tel que x est dans A et f(x)=y. Pour utiliser une hypothèse yf(A), on peut fixer x tel que x est dans A et f(x)=y. L'ensemble f(A) est appelée image de A par f, on parfois image directe de A par f lorsqu'on veut insister sur la différence avec l'opération décrite dans le paragraphe suivant.

Dans l'autre sens, on peut utiliser une fonction f de X dans Y pour transporter une partie B de Y dans X. On obtient la partie notée f¹(B) et définie par f¹(B)={x|f(x)B}. Elle appelée image réciproque de B par f, ou image inverse de B par f, ou préimage de B par f. Là encore il faut se méfier beaucoup de la notation qui reprend les mêmes symbole que pour la réciproque d'une fonction. Ce n'est pas un hasard, car si f est bijective et si on note f¹ sa réciproque alors l'image inverse de B par f coïncide avec son image directe par f¹. Cependant f¹(B) est toujours bien définie, même si f n'est pas bijective.

Lean ne permet pas la notation dangereuse f(A) (ou f A) qui est remplacée par l'étrange notation f '' A ou, sans utiliser de notation, par set.image f A. De même l'image inverse ne peut pas être noté f⁻¹(B), elle est notée f ⁻¹' B ou set.preimage f B. Il faut remarquer que x ∈ f ⁻¹' B signifie f x ∈ B par définition, il n'y a rien à démontrer pour passer d'un de ces énoncés à l'autre.

Exemple

Soit f une fonction de X dans Y, et soit B et B deux parties de Y. Montrons que si BB alors f¹(B)f¹(B).

example (X Y : Type) (B₁ B₂ : set Y) (f : X  Y) :
B₁  B₂  f ⁻¹' B₁  f ⁻¹' B₂ :=
Démonstration
Supposons BB.
  intro hyp,
X Y : Type,
B₁ B₂ : set Y,
f : X  Y
 B₁  B₂  f ⁻¹' B₁  f ⁻¹' B₂
X Y : Type,
B₁ B₂ : set Y,
f : X  Y,
hyp : B₁  B₂
 f ⁻¹' B₁  f ⁻¹' B₂
Soit x dans f¹(B), montrons que x est dans f¹(B).
  intros x hx,
X Y : Type,
B₁ B₂ : set Y,
f : X  Y,
hyp : B₁  B₂
 f ⁻¹' B₁  f ⁻¹' B₂
X Y : Type,
B₁ B₂ : set Y,
f : X  Y,
hyp : B₁  B₂,
x : X,
hx : x  f ⁻¹' B₁
 x  f ⁻¹' B₂
L'hypothèse sur x signifie que f(x) est dans B
  have hfx : f x  B₁, exact hx,
X Y : Type,
B₁ B₂ : set Y,
f : X  Y,
hyp : B₁  B₂,
x : X,
hx : x  f ⁻¹' B₁
 x  f ⁻¹' B₂
X Y : Type,
B₁ B₂ : set Y,
f : X  Y,
hyp : B₁  B₂,
x : X,
hx : x  f ⁻¹' B₁,
hfx : f x  B₁
 x  f ⁻¹' B₂
Comme B est inclus dans B, f(x) est aussi dans B
  exact hyp hfx,
X Y : Type,
B₁ B₂ : set Y,
f : X  Y,
hyp : B₁  B₂,
x : X,
hx : x  f ⁻¹' B₁,
hfx : f x  B₁
 x  f ⁻¹' B₂
no goals
QED.
X Y : Type,
B₁ B₂ : set Y,
f : X  Y
 B₁  B₂  f ⁻¹' B₁  f ⁻¹' B₂

La feuille de td 4 contient des exercices sur ce cours. En étant patient, car un navigateur web n'est pas prévu pour faire tourner un assistant de démonstration, on peut travailler sur cette feuilles en ligne .

Le chapitre suivant présente les concepts de contradiction et de négation, le raisonnement par l'absurde, la contraposition...