I wonder if the propositions below are well known results in mathematical analysis literature. Any reference containing their demonstration?
Proposition. Let $X$ and $Y$ complete and separable metric spaces. If $f:X\times K\to \mathbb{R}$ a bounded upper semicontinuous function and $K\subset Y$ compact. Then
$X\ni x\longmapsto \max_{y\in K}f(x,y)\in \mathbb{R}$ is upper semicontinuous on $X$ and,
there exists a mensurable $\varphi:X\to K$ for which $$ f(x,\varphi(x))=\max_{y\in K} f(x,y). $$
This seems to be a kind of implicit function theorem. I did not find anything like that in the book of Steven G Krantz & Harold R. Parks ( link 1, link 2). I also tried to follow the referêcias I could find in the excellent post of Tao. But without success.