Dimostrare formalmente l'iniettività e la suriettività di una funzione

[GlassPrisoner91]

Probabilmente è un quesito che è stato posto più volte ma vorrei sapere come faccio a dimostrare formalmente l'iniettività o una suriettività di una funzione. Mi spiego meglio: so quando una funzione è iniettiva o suriettiva, ma non riesco a capire come dimostrare ciò su un pezzo di carta (forse la soluzione è più facile di quanto si pensi ma vorrei delle conferme da voi). Ad esempio, voglio dimostrare l'iniettività di questa funzione:

$f: NN \to NN$ tale che $f(n) = 2^(2^n)$

Detto in parole povere, so che una funzione è iniettiva quando ogni elemento del dominio ha un immagine diversa. In questo caso, correggetemi se sbaglio, procedendo per tentativi abbiamo che:

$f(1) = 2^(2^1) = 4$
$f(2) = 2^(2^2) = 16$
$f(3) = 2^(2^3) = 256$
$f(4) = 2^(2^4) = 65.536$
...e così via.
Quindi è facile notare che le immagini saranno sempre diverse, pertanto la funzione è iniettiva. Ora mi chiedo, una dimostrazione del genere può andar bene? O è poco formale ecc.?

[adaBTTLS1]

si potrebbe procedere in vari modi, come ad esempio mostrando come ottieni il singolo termine dal precedente, dalla stretta monotonia, ma in questo caso penso sia più semplice procedere "per assurdo" o dalla definizione:
$"se "m,n in NN$ (se procedessi p.a. potresti aggiungere $"con "m != n$), supponiamo che sia $f(m)=f(n)," cioè "2^(2^m)=2^(2^n)." allora ... sarà "2^m=2^n " e pertanto "m=n$