EDB — 1Z1

[1Z1]Prerequisiti:[1Z0]↺↻. (Proposto il 2023-01-17)

Supponiamo che $X$ non abbia massimo; sia $S$ definito come in [1Z0]↺↻; si dimostri che è una funzione iniettiva

e che $S(x)\ne 0_X$, per ogni $x$ (cioè, $0_X$ non è successore di nessun elemento).

Notiamo che in generale $S$ non sarà surgettiva come funzione $S:X\to X⧵\{0_X\}$: vi potrebbero essere altri elementi $y\in S,y\ne 0_X$ che non sono successori di alcun elemento. Se però, dato $y\in X$, esiste $x\in X$ per cui $y=S(x)$, diremo che $x$ è il predecessore di $y$.