Let us start with the following well-known definition:
Definition 1. Let $C\subseteq A^n$ be a code over $A$ and let $t\in \Bbb Z^+$ be a positive integer. We say that the code $C$ is $\boldsymbol t$-error correcting if nearest neighbour decoding is able to correct at most $t$ errors, assuming that if a tie occurs in the decoding process, a decoding error is reported. That is, if whenever $x \in C$ and $y\in A^n$ such that $\mathrm{d}(x,y)\leq t$, then $y$ is decoded to $x$ using nearest neighbour decoding.
Now let us make an observation.
Remark. Recall that when there is no unique nearest codeword to $x\in C$, then nearest neighbour decoding fails. So, a code $C\subseteq A^n$ is $t$-error correcting if and only if whenever $y\in A^n$ is a word within distance $t$ of a codeword $x\in C$ (that is, $\mathrm{d}(x,y)\leq t$), then $$\mathrm{d}(x,y) < \mathrm{d}(z,y), \quad \text{for all } x\neq z \in C.$$
The Remark gives us a more abstract way to state the definition of $t$-error correcting without mentioning nearest neighbour decoding.
However, I stumbled on another statement of the definition (which I found on some lecture notes on the web):
Definition 2. The code $C$ is $t$-error correcting if there do not exist $x,z \in C$ such that $x\neq z$ and $y\in A^n$ such that $$\mathrm d(x, y)\leq t, \quad \mathrm d (z, y)\leq t.$$
My question is why the last definition is equivalent to the first one (given with the form of the remark).
Could you please give me a hand?
UPDATE: My attempt: Definition 1 tells us that $$(\forall x\in C)(\forall z \in C)(\forall y\in A^n)(d(x,y)\leq t)(z\neq x \implies d(x,y)<d(z,y)).$$
Definition 2 tells us that $$(\forall x\in C)(\forall z \in C)(\forall y\in A^n)(d(x,y)\leq t)(d(z,y)\leq t \implies z=x).$$ Equivalently, $$(\forall x\in C)(\forall z \in C)(\forall y\in A^n)(d(x,y)\leq t)(z\neq x\implies d(z,y)>t ).$$ Equivalently, $$(\forall x\in C)(\forall z \in C)(\forall y\in A^n)(d(x,y)\leq t)(z\neq x\implies d(z,y)>t\geq d(x,y)).$$ So the Def2 $\implies$ Def 1. Is that correct? How about $\Longleftarrow$?