Doppia implicazione stretta monotonia

[DavideGenova1]

Ciao, amici!
Il mio testo di analisi definisce una funzione f strettamente monotona crescente (o descrescente) in D come una funzione tale che
$AAx_1,x_2 in D, x_1 f(x_1) f(x_1)>f(x_2)$ per la strettamente descrescente).
Ora, dato che, utilizzando il fatto che $(A=>B)<=>(not B => not A)$, direi che (tratto per brevità solamente la strettamente crescente)
$AAx_1,x_2 in D, not (f(x_1) not (x_1=f(x_2) => x_1>=x_2$, il che mi pare non possa significare altro che
$f(x_1)>f(x_2) => x_1>x_2$ (e anche $f(x_1)=f(x_2) => x_1=x_2$, anzi $f(x_1)=f(x_2) <=> x_1=x_2$ per la definizione di funzione)
perché l'implicazione $f(x_1)>f(x_2) => x_1=x_2$ negherebbe la definizione stessa di funzione e $f(x_1)=f(x_2) => x_1>x_2$ contraddirebbe la tesi $x_1>x_2 => f(x_1)>f(x_2)$.
Quindi direi che valga la doppia implicazione
$AAx_1,x_2 in D, x_1 f(x_1) f(x_1)>f(x_2)$ per la strettamente descrescente)...
Giusto...? o no? A me sembrerebbe ovvio, ma quando qualcosa sembra ovvia non è affatto impossibile che non sia affatto vera...
Grazie di cuore a tutti!

EDIT: sostituita l'espressione "negando l'implicazione" con "utilizzando il fatto che $(A=>B)<=>(not B => not A)$" e corrette (spero) alcune cosette grazie all'aiuto di Gi8: grazie!!!

[Gi81]

Guarda che la negazione di $AA x_1,x_2 in D, x_1< x_2 => f(x_1)
E' piuttosto: $ EE x_1,x_2 in D$ tali che $x_1 < x_2 ^^ f(x_1)>=f(x_2)$

[DavideGenova1]

Grazie di cuore, Gi8! Quello che volevo dire è che intendevo utilizzare l'equivalenza tra $A=>B$ e $not B => not A$, che credo valga anche in un caso come il mio $AAn, p$ con $(A=>B)$ come proposizione p, cioè del tipo $(AAn, (A=>B)) <=> (AAn, (not B => not A))$... o sbaglio?
Grazie ancora!!!

[Gi81]

Non sbagli. La tua richiesta è
"La definizione di funzione strettamente crescente è $AA x_1,x_2 in D, x_1 < x_2 => f(x_1) < f(x_2)$.
Posso dire che ciò è equivalente a $AA x_1,x_2 in D, x_1 < x_2 <=> f(x_1) < f(x_2)$?"

Risposta: sì.
Motivo: quello che hai scritto tu

[DavideGenova1]

$+oo$ grazie, Gi8!!!