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 $x ∈ A$ 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 $R ∈ R$, mais alors $R ∉ R$ par définition de $R$, soit $R ∉ R$, ce qui entraînerait $R ∈ R$ 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 : $P x$ si et seulement si $x ∈ A$. Autrement dit, pour tout $x$, $P$ associe à $x$ l'énoncé $x ∈ A$. 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 | P x\}$. 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 | P x\}$. 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, x ∈ A ⇔ x ∈ B$. 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 $∀ x ∈ A, P x$ est l'abréviation de $∀ x, x ∈ A ⇒ P x$. De même la formule $∃ x ∈ A, P x$ est l'abréviation de $∃ x, x ∈ A \text{ et } P x$.

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.

example : 8 ∈ { n | ∃ k, n = 2*k} :=

  use 4,

⊢ 8 ∈ {n : ℕ | ∃ (k : ℕ), n = 2 * k}

⊢ 8 = 2 * 4

  ring,

⊢ 8 = 2 * 4

no goals

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, x ∈ A ⇒ x ∈ B$. On note cela $A ⊂ B$ ou $A ⊆ B$. 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 $A ⊊ B$.

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

Pour démontrer (directement) $A ⊂ B$, 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.

example : {n | ∃ k, n = 8*k} ⊆ {n | ∃ k, n = 4*k} :=

  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}

  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}

  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)

  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

Le principe d'extensionnalité montre que, pour démontrer une égalité d'ensembles $A = B$, il suffit de montrer $A ⊂ B$ et $B ⊂ A$. 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 $A ∩ B$. Si $A$ et $B$ correspondent aux prédicats $P$ et $Q$ respectivement alors le prédicat correspondant à $A ∩ B$ associe à $x$ l'énoncé « $P x \text{ et } Q x$ ». Pour démontrer que $x$ est dans $A ∩ B$, 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 $A ∩ B$, 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.

example (X : Type) (A B : set X) : A ∩ B ⊆ B :=

  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

  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

  exact hxB,

X : Type,
A B : set X,
x : X,
hxA : x ∈ A,
hxB : x ∈ B
⊢ x ∈ B

no goals

La réunion de $A$ et $B$ est l'ensemble des objets qui sont soit dans $A$ soit dans $B$. On le note $A ∪ B$. Si $A$ et $B$ correspondent aux prédicats $P$ et $Q$ respectivement alors le prédicat correspondant à $A ∪ B$ associe à $x$ l'énoncé « $P x \text{ ou } Q x$ ». Pour démontrer (directement) que $x$ est dans $A ∪ B$, 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 $A ∪ B$, 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.

example (X : Type) (A B : set X) : A ⊆ A ∪ B :=

  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

  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

  exact hxA,

X : Type,
A B : set X,
x : X,
hxA : x ∈ A
⊢ x ∈ A

no goals

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 $\mathrm{Id}_X$, 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) = x^2$. Pour parler de cette fonction sans la nommer, les mathématiciens utilisent le plus souvent la notation $x ↦ x^2$, qui se lit « $x$ va sur $x^2$ » ou « la fonction qui envoie $x$ sur $x^2$ ». 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, x^2$, 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 $u_0 = 1$ et $u_{n+1} = sin(u_n)$ » définit sans ambiguïté une suite de nombre réels mais on ne peut pas donner d'expression de $u_n$ 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 : X → Y$ et $g : Y → Z$ des fonctions alors la fonction $g ∘ f$ 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 $Y^X$ ou $X → Y$, 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 ↦ (y ↦ xy)$. À 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 \text{ 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 = g ⇔ ∀ x, f(x) = g(x)$.

On dit qu'un fonction $f$ de $X$ dans $Y$ est injective si $∀ x\; x' ∈ X, f(x) = f(x') ⇒ x = x'$. On dit qu'elle est surjective si $∀ y ∈ Y, ∃ x ∈ X, 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 $g ∘ f = \mathrm{Id}_X$ et $f ∘ g = \mathrm{Id}_Y$. 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.

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') :=

  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'

  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'

  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'

  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'

  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

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 \,|\, ∃ x ∈ A, 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 $y ∈ f(A)$, il faut fournir $x$ tel que $x$ est dans $A$ et $f(x) = y$. Pour utiliser une hypothèse $y ∈ f(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.

example (X Y : Type) (B₁ B₂ : set Y) (f : X → Y) :
B₁ ⊆ B₂ → f ⁻¹' B₁ ⊆ f ⁻¹' B₂ :=

  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₂

  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₂

  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₂

  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

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 là.

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