Suppose $f$ and $g$ are functions. I am pretty sure that the definition of big-O has its definition conform to the following logical structure
$$\exists \, k \, \exists C \, \forall \,x\, :\, x > k \implies|f(x)| \leq C|g(x)|$$
since it also conforms to proper usage when attempting to prove by contradiction that $f$ is not big-O of $g$, but I would like confirmation.
Thanks!
Yes, this is correct. Under the assumption that you surely want to make that we are talking about what it means that $f$ is $O(g)$ as $x \to \infty$ (and not some other point, or still something else).
More generally, $f$ is $O(g)$ on $S$ means that there exists some $C$ such that $|f(x)| \le C |g(x)|$ for all $x \in S$ (equivalently $x \in S $ implies $|f(x)| \le C |g(x)|$).
And, $f$ is $O(g)$ as $x \to p$ means that there exists some open neighborhood $U$ of $p$ and a $C$ (that may depend on $U$) such that $|f(x)| \le C |g(x)|$ for all $x \in U$ (equivalently $x \in U $ implies $|f(x)| \le C |g(x)|$).
The sets $\{ x \in \mathbb{R} \colon x >k\}$ are a basis of the open neighborhoods of $+\infty$. This second statement is thus equivalently to what you said.
In particular, it is more coherent to choose the neighborhood first and then the constant. But in the particular case you could also invert the order of the existential quantifiers and it would not yield a different definition in this case.