construire des birestrictions avec des jectivités spécifiques

• Son injectivité : \(\forall x\in I.\forall y\in I.(f(x)=f(y)\implies x=y).\)
• Sa surjectivité : \(\forall y\in J.\exists x\in I.f(x)=y.\)
• Sa bijectivité : injective et surjective simultanément.
• Être aucun de ces précédents.

Preuve    \(f\big|_\varnothing^\varnothing\) est de type \(\varnothing\to\varnothing.\) Ainsi, elle est injective si et seulement si : $$\forall x\in\varnothing.\forall y\in\varnothing.(f(x)=f(y)\implies x=y)$$ C'est vrai par principe d'explosion. De même, c'est surjectif si et seulement si : $$\forall y\in\varnothing.\exists x\in\varnothing.f(x)=y$$ C'est également vrai par principe d'explosion. \(f\) est alors à la fois injective et surjective, ce qui prouve donc sa bijectivité. \(\blacksquare\)

Preuve    \(f\big|_\varnothing^{\{*\}}\) est de type \(\{*\}\to\varnothing.\) Ainsi, elle est injective si et seulement si : $$\forall x\in\varnothing.\forall y\in\varnothing.(f(x)=f(y)\implies x=y)$$ C'est vrai par explosion. Cependant, elle est surjective si et seulement : $$\forall y\in\{*\}.\exists x\in\varnothing.f(x)=y$$ Or, \(\exists x\in\varnothing.f(x)=*\) est toujours faux, d'où sa non-surjectivité. \(\blacksquare\)

Proof    Par manipulation algébrique, \begin{equation*} \begin{split} &\neg\forall x\in I.\forall y\in I.(f(x)=f(y)\implies x=y)\\ \dashv\vdash &\exists x\in I.\neg\forall y\in I.(f(x)=f(y)\implies x=y)\text{ par conversion des quantificateurs}\\ \dashv\vdash &\exists x\in I.\exists y\in I.\neg(f(x)=f(y)\implies x=y)\text{ par }\!\!\left\{\!\!\begin{array}{ll}\text{conversion des quantificateurs}\\\text{covariance de la dernière composante des formules existentielles}\end{array}\right.\\ \dashv\vdash &\exists x\in I.\exists y\in I.\neg(\neg f(x)=f(y)\vee x=y)\text{ par }\!\!\left\{\!\!\begin{array}{ll}\text{implication matérielle}\\\text{contravariance de la négation}\\\text{covariance de la dernière composante des formules existentielles}\end{array}\right.\\ \dashv\vdash &\exists x\in I.\exists y\in I.(\neg\neg f(x)=f(y)\land\neg x=y)\text{ par }\!\!\left\{\!\!\begin{array}{ll}\text{lois de De Morgan}\\\text{covariance de la dernière composante des formules existentielles}\\\text{covariance des composantes de la conjonction}\end{array}\right.\\ \dashv\vdash &\exists x\in I.\exists y\in I.(f(x)=f(y)\land\neg x=y)\text{ par }\!\!\left\{\!\!\begin{array}{ll}\text{élimination de la double négation}\\\text{covariance de la dernière composante des formules existentielles}\\\text{covariance des composantes de la conjonction}\end{array}\right.\\ \dashv\vdash &\exists x\in I.\exists y\in I.(\neg x=y\land f(x)=f(y))\text{ par }\!\!\left\{\!\!\begin{array}{ll}\text{commutativité de la conjonction}\\\text{covariance de la dernière composante des formules existentielles}\end{array}\right. \end{split} \end{equation*} Soit \(x,y\in I\) tel que \(\neg x=y\) et \(f(x)=f(y).\) Si on définit \(*:=f(x)=f(y)\in J,\) cela assure que \(f^{-1}(\{*\})\) ait au moins un élément, \(x\) et \(y.\) Ainsi, \(|f^{-1}(\{*\})|\ge2.\) \(\blacksquare\)

Proof    \(f\big|_{\{x,y\}}^{\{*\}}\) est non-injective, car \(f(x)=*=f(y)\) alors que \(x\ne y.\) Cependant, elle est surjective, car son image \(f\big|_{\{x,y\}}^{\{*\}}(\{x,y\})=\{f(x),f(y)\}=\{*\}\) est son codomaine. \(\blacksquare\)

Preuve    \(f\big|_{\{x,y\}}^{\{*\}}\) est non-injective, car \(f(x)=*=f(y)\) tandis que \(x\ne y.\) Elle n'est pas non plus surjective, car \(f\big|_{\{x,y\}}^{\{*,\{*\}\}}(\{x,y\})=\{f(x),f(y)\}=\{*\}\) est un sous-ensemble strict de son codomaine \(\{*,\{*\}\},\) car \({*}\ne\{*\}\) à cause d'un tristement célèbre corollaire de l'axiome de régularité.

• Bijective quand \(I=\varnothing\) et \(J=\varnothing,\)
• Injective non-surjective with \(I=\varnothing\) et \(J=\{*\},\)
• Surjective non-injective with \(I=\{-\pi,\pi\}\) et \(J=\{\pi^2\},\)
• Ni l'une ni l'autre si \(I=\{-\pi,\pi\}\) et \(J=\{\pi^2,\{\pi^2\}\}.\)

• \(|I_0|\ge0\) et \(|J_0|\ge0\) si la birestriction est bijective.
• \(|I_0|\ge0\) et \(|J_0|\ge1\) si la birestriction est injective non-surjective,
• \(|I_0|\ge2\) et \(|J_0|\ge1\) si la birestriction est surjective non-injective,
• \(|I_0|\ge2\) et \(|J_0|\ge2\) si la birestriction est non-injective non-surjective.

Preuve

• Chaque ensemble est de cardinalité au moins nulle, ce qui trivialise la première affirmation. Utiliser \(I_0=J_0=\varnothing\) fonctionne toujours, grâce au théorème 1.1. \(\Box\)
• Par loi du tiers exclu, \(|I_0|\ne0\) ou \(|I_0|=0.\) Si \(|I_0|\ne0,\) alors \(|J_0|\ne0\) car il n'y a pas de fonction d'un ensemble non-vide vers l'ensemble vide. Si \(|I_0|=0\) et \(|J_0|=0,\) alors \(I_0=J_0=\varnothing,\) ce qui conduit à une birestriction bijective qui, du coup, n'est pas non-surjective ; ainsi, si \(|I_0|=0,\) on a \(|J_0|\ne0.\) Par élimination de la disjonction, on a que \(|J_0|\ne0,\) ou en d'autres mots, \(|J_0|\ge1.\) \(\Box\)
• Par le lemme 1.3, la non-injectivité de \(f\big|_{I_0}^{J_0}\) requiert l'existence de \(*\in J_0,\) telle que \(|J_0|\ge1,\) et telle que \(\big(f\big|_{I_0}^{J_0}\big)^{-1}(\{*\})\) ait au moins deux éléments distincts. Puisque \(\big(f\big|_{I_0}^{J_0}\big)^{-1}(\{*\})\) est, par définition, une partie de \(I_0,\) on a que \(I_0\) a également au moins deux éléments, dont précisément les mêmes ; ainsi, \(|I_0|\ge2.\) En tout et pour tout, on a alors que \(|I_0|\ge2\) et \(|J_0|\ge1.\) \(\Box\)
• Comme démontré dans le précédent point, la non-injectivité de \(f\big|_{I_0}^{J_0}\) requiert \(|I_0|\ge2\) et \(|J_0|\ge1.\) Cependant, si \(|I_0|\ge2\) et \(|J_0|=1,\) alors si l'on prend \({!}\in I_0,\) on a effectivement que pour tout \(*\in J_0,\) on a \(f(!)=*,\) ce qui démontre sa surjectivité. Si on veut que ce soit ni injectif ni surjectif, il faut alors que l'on ait \(|J_0|\ge2.\) En tout et pour tout, une telle birestriction doit satisfaire \(|I_0|\ge2\) et \(|J_0|\ge2.\) \(\blacksquare\)

Preuve    Par définition, \(f(I)\) est l'ensemble des images des éléments de \(I\) par \(f,\) ce qui garantit sa surjectivité. \(\blacksquare\)

Preuve    Par non-injectivité de \(f,\) il y a \(x,y\in I\) tels que \(x\ne y\) et \(f(x)=f(y).\) Alors, \(f\big|_I^{f(I)}(x)=f\big|_I^{f(I)}(y),\) bien que \(x\ne y,\) ce qui prouve sa non-injectivité. \(\blacksquare\)

Preuve    \(f\big|_I^{f(I)}\) est déjà non-injective et surjective grâce au théorème 1.8, mais \(f(I)\not\in f(I)\) par le même corollaire de l'axiome de régularité que celui susmentionné, d'où que \(f\big|_I^{f(I)\cup\{f(I)\}}\) est ni injective ni surjective. \(\blacksquare\)