QuantumInfo.ForMathlib.Misc

Let $\alpha$ be a type equipped with a top element $\top$. For any decidable proposition $h$ and elements $x, y \in \alpha$, if $x \neq \top$ and $y \neq \top$, then the conditional expression $\text{if } h \text{ then } x \text{ else } y$ is also not equal to $\top$.

Let $f: I \to \alpha$ be a family of elements in a conditionally complete lattice $\alpha$. If for all $i \in I$, the values $f(i)$ are contained within the closed interval $[a, b]$, then the supremum of the family of subtypes $\langle f(i), h(i) \rangle$ in the interval $[a, b]$ has a underlying value equal to the supremum of the original family $f(i)$ in $\alpha$. That is, $(\sup_{i} \langle f(i), h(i) \rangle).val = \sup_{i} f(i)$.

Let $f: I \to \alpha$ be a family of elements in a conditionally complete lattice $\alpha$. If for all indices $i \in I$, the value $f(i)$ lies in the closed interval $[a, b]$, then the supremum of these elements as members of the subtype $[a, b]$ is equal to the supremum of the values $f(i)$ in $\alpha$, considered as an element of the subtype $[a, b]$. Specifically, if $h: \forall i, f(i) \in [a, b]$, then $\sup_i \langle f(i), h(i) \rangle = \langle \sup_i f(i), h' \rangle$, where $h'$ is the proof that $\sup_i f(i) \in [a, b]$ derived from the bounds $a$ and $b$.

Let $f$ be a family of elements indexed by $i$ such that each $f_i$ lies within the closed interval $[a, b]$, i.e., $f_i \in \{x \mid a \leq x \leq b\}$. Let $\langle f_i, h_i \rangle$ denote the corresponding elements regarded as members of the subtype associated with the set $[a, b]$. Then the value of the infimum of these elements in the subtype is equal to the infimum of the original values $f_i$ in the parent type: $$\left( \textstyle\inf_i \langle f_i, h_i \rangle \right).\text{val} = \textstyle\inf_i f_i$$

Let $f: I \to [a, b]$ be a family of elements indexed by $i \in I$ such that for all $i$, $f(i)$ belongs to the closed interval $[a, b] \subset \mathbb{R}$. Let $\langle f(i), h(i) \rangle$ denote the representation of $f(i)$ as an element of the subtype $[a, b]$. Then the infimum of this family taken within the subtype $[a, b]$ is equal to the infimum of the values $f(i)$ taken in the carrier type, i.e., $\inf_{i} f(i)$, and this infimum is itself contained within the interval $[a, b]$. Specifically, $a \le \inf_i f(i) \le b$ holds.

Let $\alpha$ be a type and $l$ be a filter on $\alpha$. Let $f, g: \alpha \to \overline{\mathbb{R}}_{\geq 0}$ be sequences (or functions) and $b \in \overline{\mathbb{R}}_{\geq 0}$ be a constant such that $b \neq \infty$. If $f$ tends to $0$ along the filter $l$ (i.e., $f \xrightarrow[l]{} 0$) and $g(x)$ is eventually bounded by $b$ in $l$ (i.e., for almost all $x$ with respect to $l$, $g(x) \leq b$), then the product $f(x) \cdot g(x)$ also tends to $0$ along $l$.

Let $s$ and $t$ be sets of real numbers. Suppose that both $s$ and $t$ are non-empty ($s \neq \emptyset$ and $t \neq \emptyset$) and consist only of non-negative elements (for all $x \in s$, $x \ge 0$, and for all $y \in t$, $y \ge 0$). Then the infimum of the product set $s \cdot t = \{z \mid \exists x \in s, y \in t, z = x \cdot y\}$ is equal to the product of their individual infima: $$\inf(s \cdot t) = \inf(s) \cdot \inf(t)$$

Let $\alpha$ and $\beta$ be types where $\alpha$ is a finite type (represented by the `Fintype` instance). For two functions $f, g: \alpha \to \beta$, the multiset of values obtained by applying $f$ to all elements in the universe of $\alpha$ is equal to the multiset of values obtained by applying $g$ to the same universe if and only if there exists a bijection $e: \alpha \simeq \alpha$ such that $f = g \circ e$.

Let $\alpha$ and $\beta$ be finite types and let $\gamma$ be a type with decidable equality. Let $f: \alpha \to \gamma$ and $g: \beta \to \gamma$ be two functions. If the multiset of values of $f$ over all elements of $\alpha$ is equal to the multiset of values of $g$ over all elements of $\beta$, then there exists a bijection $e: \alpha \simeq \beta$ such that $f = g \circ e$.