QuantumInfo.ForMathlib.ContinuousSup

Let $S$ be a subset of a topological space $\beta$, and let $f: \beta \to \alpha$ be a continuous function into a conditionally complete linear order $\alpha$. If the closure of $S$, denoted by $\overline{S}$, is compact, then the supremum of the image of $S$ under $f$ is equal to the supremum of the image of the closure of $S$ under $f$. That is, $\sup(f(S)) = \sup(f(\overline{S}))$.

Let $f: \beta \to \alpha$ be a continuous function. If the closure of a subset $S \subseteq \beta$ is compact, then the infimum of the image of $S$ under $f$ is equal to the infimum of the image of the closure of $S$ under $f$, i.e., $\inf(f(S)) = \inf(f(\overline{S}))$.

Let $S$ be a set in a topological space such that its closure $\text{cl}(S)$ is compact. Let $f: X \times \beta \to \alpha$ be a continuous function (where $\alpha$ is a conditionally complete linear order with a compatible topology). Then the map $x \mapsto \sup \{f(x, y) \mid y \in S\}$ is continuous.

Let $S$ be a set such that its closure $\overline{S}$ is compact. Let $f : X \times Y \to \mathbb{R}$ (or more generally, a continuous function into a conditionally complete lattice with a compatible topology) be a continuous function. Then the function $x \mapsto \inf_{y \in S} f(x, y)$ is continuous.

Let $S$ be a set such that its closure $\overline{S}$ is compact. If $f(x, y)$ is a continuous function of two variables (where $\upharpoonleft f$ denotes the uncurried version of $f$), then the function $g(x) = \sup_{y \in S} f(x, y)$ is continuous.

Let $S$ be a set such that its closure $\overline{S}$ is compact. Let $f$ be a continuous function of two variables (jointly continuous in $x$ and $y$). Then the function defined by the infimum over $S$, $x \mapsto \inf_{y \in S} f(x, y)$, is also continuous.

Let $S$ be a bounded set in the bornology of a space. If a function $f(x, y)$ is jointly continuous (denoted by the continuity of its uncurled form $\intprod f$), then the function mapping $x$ to the supremum of the image of $S$ under $f(x, \cdot)$, given by $x \mapsto \sup \{f(x, y) \mid y \in S\}$, is continuous.

Let $S$ be a set that is bounded in the bornology of the space. Let $f(x, y)$ be a function that is continuous in both variables (jointly continuous). Then the function defined by the infimum of the image of $S$ under $f$ at each point $x$, given by $x \mapsto \inf \{f(x, y) \mid y \in S\}$, is a continuous function of $x$.

Let $S$ be a bounded set in a bornological space. Let $f$ be a function such that the uncurried version $\text{uncurry}(f) : (x, y) \mapsto f(x, y)$ is continuous. Then the function mapping $x$ to the supremum of the values of $f$ over $S$, defined by $x \mapsto \sup_{y \in S} f(x, y)$, is continuous.

Let $S$ be a bounded set in a bornological space. Let $f(x, y)$ be a function that is jointly continuous in $x$ and $y$. Then the function defined by the infimum over $S$, $x \mapsto \inf_{y \in S} f(x, y)$, is continuous.

Let $\mathbf{k}$ be a commutative topological ring that is also a conditionally complete linear order with an order topology. Let $E$ and $F$ be modules over $\mathbf{k}$ equipped with the module topology (the finest topology making all linear maps from $\mathbf{k}$ continuous). Further assume $F$ is a finite-dimensional pseudo-metric space that is a proper space (where closed balls are compact). Let $f: E \to L(F, \mathbf{k})$ be a bilinear map. For any bounded set $S \subseteq F$, the function mapping $x \in E$ to the supremum $\sup_{y \in S} f(x, y)$ is continuous.

Let $\mathbf{k}$ be a commutative topological ring that is also a conditionally complete linear order equipped with the order topology. Let $E$ be a topological module over $\mathbf{k}$ satisfying the `IsModuleTopology` condition (meaning its topology is the finest compatible with its module structure). Let $F$ be a finite-dimensional $\mathbf{k}$-module that is also a proper pseudo-metric space and satisfies `IsModuleTopology`. Given a bilinear map $f: E \times F \to \mathbf{k}$ (represented as $f: E \to \text{Hom}(F, \mathbf{k})$) and a bounded subset $S \subseteq F$, the function defined by the infimum over $S$, $x \mapsto \inf_{y \in S} f(x, y)$, is continuous.

Let $\mathbf{k}$ be a nontrivially normed field that is also a complete space and a conditionally complete linear order equipped with the order topology. Let $E$ and $F$ be finite-dimensional topological vector spaces over $\mathbf{k}$ (specifically, $E$ and $F$ are finite-dimensional modules with continuous scalar multiplication, $T_2$ separation, and compatible topological group structures). Let $f: E \to (F \to \mathbf{k})$ be a bilinear map (represented as a linear map from $E$ to the space of linear maps from $F$ to $\mathbf{k}$). For any bounded set $S \subseteq F$, the function $x \mapsto \sup_{y \in S} f(x, y)$ is continuous.

Let $\mathbf{k}$ be a nontrivially normed field that is also a conditionally complete linear order equipped with the order topology and is a complete space. Let $E$ and $F$ be finite-dimensional topological vector spaces over $\mathbf{k}$ (specifically, Hausdorff topological additive groups with continuous scalar multiplication). Let $F$ also be a pseudo-metric space and a proper space. Given a bilinear map $f: E \to L(F, \mathbf{k})$ (represented as a linear map from $E$ to the space of linear maps from $F$ to $\mathbf{k}$) and a bounded subset $S \subseteq F$, the function $x \mapsto \inf_{y \in S} f(x)(y)$ is continuous from $E$ to $\mathbf{k}$.

Let $\mathbb{k}$ be an $\mathbb{R}$-clike field (such as $\mathbb{R}$ or $\mathbb{C}$) that is also a conditionally complete linear order with the order topology. Let $E$ be a finite-dimensional inner product space over $\mathbb{k}$ that is a proper space. Let $f: E \times E \to \mathbb{k}$ be a bilinear form, and let $S \subseteq E$ be a bounded set. Then the function $x \mapsto \sup_{y \in S} f(x, y)$ is continuous.

Let $\mathbf{k}$ be an $\mathbb{R}$-isomorphic complete field (specifically an `RCLike` field such as $\mathbb{R}$ or $\mathbb{C}$) equipped with a conditionally complete linear order, the order topology, and let $E$ be a finite-dimensional inner product space over $\mathbf{k}$ that is also a proper metric space. Given a bilinear form $f: E \times E \to \mathbf{k}$ and a bounded subset $S \subseteq E$, the function $x \mapsto \inf_{y \in S} f(x, y)$ is continuous.

Let $F, E,$ and $G$ be normed spaces, and let $f: F \to \mathcal{L}(E, G)$ be a continuous semilinear map. If $S \subseteq E$ is a bounded set in the sense of bornology, then the function mapping $x$ to the supremum of $f(x, y)$ over $y \in S$ is continuous. That is, the map $x \mapsto \sup_{y \in S} f(x, y)$ is continuous.

Let $E$, $F$, and $G$ be topological vector spaces and $f: F \to \mathcal{L}(E, G)$ be a Continuous Linear Map (or semilinear map). Let $S \subseteq E$ be a bounded set. If $h_S$ is a proof that $S$ is bounded, then the function $x \mapsto \inf_{y \in S} (f(x))(y)$ is continuous.

Let $E$ be a finite-dimensional real inner product space. Let $f: E \times E \to \mathbb{R}$ be a bilinear form and $S \subseteq E$ be a bounded set. Then the function mapping $x \in E$ to the supremum $\sup_{y \in S} f(y, x)$ is continuous.

Let $E$ be a finite-dimensional real inner product space. Let $f: E \times E \to \mathbb{R}$ be a bilinear form and $S \subseteq E$ be a bounded set. Then the function mapping $x \in E$ to the infimum of the values of the bilinear form with respect to its first argument over $S$, defined by $x \mapsto \inf_{y \in S} f(y, x)$, is continuous.