I was studying measure theory and now I'm going to probability. I know the usual definitions of joint and marginal CDF's. But I'm particularly interested to define these concepts looking the probability as a measure. To do so, I wrote the following.
Let $(\Omega,\mathcal{A},P)$ be a probability space and let $X,Y:\Omega \rightarrow \mathbb{R}$ be random variables. Define the joint distribution function as $F_{XY}(x,y)=P_{XY}((-\infty,x]\times (-\infty,y])=P\{X(w)\leq x,Y(w)\leq y\}$, where $P_{XY}: \mathcal{B}_{\mathbb{R}^2}\rightarrow [0,1]$ is the joint probability distribution (or the pushforward measure) of $X$ and $Y$. Given the joint distribution function $F_{XY}$, the marginal distribution function of $X$ is defined as $F_X(x)=P_{XY}\{(-\infty,x]\times\mathbb{R}\}$
I would like to read your comments on my definitions. Specially, if they are correctly defined.
Thanks!