Preimages, Unions and Intersections over an Index Set, Suprema and Infima, and Superlevel Sets as Typed Terms

This helper adopts the setting of Measure Spaces, Borel Sets and Lebesgue Measure on the Real Line: Standing Notation; it is a statement of the metatheory about expressions. Let $k\ge0$, the distinct set variables $x_{1},\dots,x_{k}$, the parameters with their fixed values, and assignments be as in Conditions Expressed by a Predicative Formula, and Guards (i); let $\gamma$ be a guard; and let terms under $\gamma$ and their values, terms of type $A$ under $\gamma$ for a class $A$, and conditions expressed by a predicative formula be as in Terms and Typed Terms under a Guard (i), Terms and Typed Terms under a Guard (ii) and Conditions Expressed by a Predicative Formula, and Guards (ii). For sets $A$ and $B$, $B^{A}$ is the set of maps $A\to B$ and $\mathcal{P}(A)$ the power set of $A$, as in Sets and Maps: Ordinary Notation (v) and The Union Set and the Power Set of a Set (ii). A variable, or a parameter, whose sets lie in a class $A$ is a term of type $A$ by Typed Terms under a Predicative Guard: Variables, Parameters, Values of Maps and Ordered Pairs, and Predicative Equations and Memberships between Them (i) and Typed Terms under a Predicative Guard: Variables, Parameters, Values of Maps and Ordered Pairs, and Predicative Equations and Memberships between Them (ii), so the terms below may be such variables. For a parameter $F$ whose value is a map $F:A\times B\to C$ and terms $s$ and $t$, $F(s,t)$ stands for the term $F((s,t))$ of Typed Terms under a Predicative Guard: Variables, Parameters, Values of Maps and Ordered Pairs, and Predicative Equations and Memberships between Them (iii) and Typed Terms under a Predicative Guard: Variables, Parameters, Values of Maps and Ordered Pairs, and Predicative Equations and Memberships between Them (iv), written with $F$, $s$ and $t$.

(i) Let $S$ and $T$ be sets. There is exactly one map $\mathrm{pre}_{S,T}:T^{S}\times\mathcal{P}(T)\to\mathcal{P}(S)$ with $\mathrm{pre}_{S,T}(f,V)=f^{-1}(V)$, the preimage of Sets and Maps: Ordinary Notation (vii), for all $f\in T^{S}$ and $V\in\mathcal{P}(T)$; here $f^{-1}(V)$ is the defined set symbol of Preimages under a Map: Membership, the Preimage Map, Sequences of Preimages, and the Set of Sets with Preimage in a Given Set (i). Let $u$ be a term of type $T^{S}$ under $\gamma$ and $B$ a term of type $\mathcal{P}(T)$ under $\gamma$, and let $u^{-1}(B)$ stand for the term $\mathrm{pre}_{S,T}(u,B)$, written with a parameter whose value is $\mathrm{pre}_{S,T}$; its value under each assignment satisfying $\gamma$ is $f^{-1}(V)$ for the values $f$ of $u$ and $V$ of $B$. Then $u^{-1}(B)$ is a term of type $\mathcal{P}(S)$ under $\gamma$.

(ii) Let $X$ and $Z$ be sets, let $I$ be a term of type $\mathcal{P}(Z)$ under $\gamma$, and let $i$ be a set variable that is none of $x_{1},\dots,x_{k}$, is not free in $\gamma$ and does not occur in $I$. Let $\gamma'$ be a guard for the variables $x_{1},\dots,x_{k},i$ that expresses the condition $\gamma\wedge i\in I$ on $x_{1},\dots,x_{k},i$; such a guard exists. Let $t$ be a term of type $\mathcal{P}(X)$ under $\gamma'$. Under an assignment of sets to $x_{1},\dots,x_{k}$ satisfying $\gamma$, write $I$ also for the value of $I$, and for $a\in I$ let $t(a)$ be the value of $t$ when $a$ is assigned to $i$ and $x_{1},\dots,x_{k}$ keep their sets. For the intersection, suppose moreover that the value of $I$ is nonempty under every assignment satisfying $\gamma$. Then there is a term $\bigcup_{i\in I}t$ under $\gamma$ and, under that supposition, a term $\bigcap_{i\in I}t$ under $\gamma$, each written with $I$, $i$ and $t$, $i$ bound in it, whose values under each assignment satisfying $\gamma$ are the class of the sets lying in $t(a)$ for some $a\in I$, respectively the class of the sets lying in $t(a)$ for every $a\in I$. For every family $(A_{a})_{a\in I}$ with $A_{a}=t(a)$ for every $a\in I$, these values are its union and intersection. Each of $\bigcup_{i\in I}t$ and $\bigcap_{i\in I}t$ is a term of type $\mathcal{P}(X)$ under $\gamma$.

(iii) Let $X$ be a set. There is exactly one map $\cup_{X}:\mathcal{P}(X)\times\mathcal{P}(X)\to\mathcal{P}(X)$ with $\cup_{X}(v,w)=v\cup w$ for all $v,w\in\mathcal{P}(X)$, and likewise exactly one map $\cap_{X}$, respectively $\setminus_{X}$, with the value $v\cap w$, respectively $v\setminus w$, with the union, intersection and difference. Let $A$ and $B$ be terms of type $\mathcal{P}(X)$ under $\gamma$, and let $A\cup B$, $A\cap B$ and $A\setminus B$ stand for the terms $\cup_{X}(A,B)$, $\cap_{X}(A,B)$ and $\setminus_{X}(A,B)$, each written with a parameter whose value is the map named; their values under each assignment satisfying $\gamma$ are the union, intersection and difference of the values of $A$ and $B$. Then $A\cup B$, $A\cap B$ and $A\setminus B$ are terms of type $\mathcal{P}(X)$ under $\gamma$.

(iv) There is exactly one map $\mathrm{Sup}:\mathcal{P}([-\infty,\infty])\to[-\infty,\infty]$ with $\mathrm{Sup}(e)=\sup e$, and exactly one map $\mathrm{Inf}:\mathcal{P}([-\infty,\infty])\to[-\infty,\infty]$ with $\mathrm{Inf}(e)=\inf e$, for every $e\in\mathcal{P}([-\infty,\infty])$, with the supremum and the infimum in $[-\infty,\infty]$ of Measure Spaces, Borel Sets and Lebesgue Measure on the Real Line: Standing Notation (ii). Let $E$ be a term of type $\mathcal{P}([-\infty,\infty])$ under $\gamma$, and let $\sup E$ and $\inf E$ stand for the terms $\mathrm{Sup}(E)$ and $\mathrm{Inf}(E)$ of Typed Terms under a Predicative Guard: Variables, Parameters, Values of Maps and Ordered Pairs, and Predicative Equations and Memberships between Them (iii), written with a parameter whose value is $\mathrm{Sup}$, respectively $\mathrm{Inf}$. Then $\sup E$ and $\inf E$ are terms of type $[-\infty,\infty]$ under $\gamma$. In particular, $E$ may be the image $\{t:i\in D\}$ of Images of Typed Terms: the Set of Values $\{t:u\in D\}$ Is a Set, Finite when $D$ Is Finite, and a Typed Term (iv), for a set variable $i$, a parameter $D$ and a term $t$ of type $B$ under the guard $\gamma\wedge i\in D$ as in that helper, with $B\subseteq[-\infty,\infty]$: by that clause it is a term of type $\mathcal{P}([-\infty,\infty])$ under $\gamma$, and by Images of Typed Terms: the Set of Values $\{t:u\in D\}$ Is a Set, Finite when $D$ Is Finite, and a Typed Term (i) its value is the set of the values of $t$ at the elements of $D$.

(v) Let $X$ be a set and let $C$ and $C'$ be subsets of $[-\infty,\infty]$, with $\le$, $<$, $\ge$ and $>$ the order of The Extended Real Line, Its Order, and [0,∞] (iii) and the relations derived from it there. There is exactly one map $\Lambda_{>}:C^{X}\times C'\to\mathcal{P}(X)$ with $\Lambda_{>}(f,c)=\{x\in X:f(x)>c\}$ for all $f\in C^{X}$ and $c\in C'$, and likewise exactly one map $\Lambda_{\ge}$, $\Lambda_{<}$, respectively $\Lambda_{\le}$, with the value $\{x\in X:f(x)\ge c\}$, $\{x\in X:f(x)<c\}$, respectively $\{x\in X:f(x)\le c\}$. Let $u$ be a term of type $C^{X}$ under $\gamma$ and $a$ a term of type $C'$ under $\gamma$, and let $\{u>a\}$, $\{u\ge a\}$, $\{u<a\}$ and $\{u\le a\}$ stand for the terms $\Lambda_{>}(u,a)$, $\Lambda_{\ge}(u,a)$, $\Lambda_{<}(u,a)$ and $\Lambda_{\le}(u,a)$, each written with a parameter whose value is the map named. Then each of these four terms is a term of type $\mathcal{P}(X)$ under $\gamma$. In particular, $C$ and $C'$ may be $[0,\infty]$, $\mathbb{R}$ or $\mathbb{Q}$, a rational number being identified with a real number as in The Real Numbers, with the Natural Numbers, Integers and Rationals Identified with Subsets of the Reals, and Completeness (v); for $p,q\in\mathbb{R}$, $p\le q$ and $p<q$ hold if and only if they hold in $\mathbb{R}$, by Order and Suprema in the Extended Real Line (i).

(vi) Let $D$ and $C$ be class variables, parameters whose values are sets, also written $D$ and $C$, and let $i$ be a set variable that is none of $x_{1},\dots,x_{k}$ and is not free in $\gamma$. Let $t$ be a term of type $C$ under the guard $\gamma\wedge i\in D$ for the variables $x_{1},\dots,x_{k},i$, and, under an assignment of sets to $x_{1},\dots,x_{k}$ satisfying $\gamma$ and for $a\in D$, let $t(a)$ be the value of $t$ when $a$ is assigned to $i$ and $x_{1},\dots,x_{k}$ keep their sets. Then under each assignment of sets to $x_{1},\dots,x_{k}$ satisfying $\gamma$ there is exactly one map $h:D\to C$ with $h(a)=t(a)$ for every $a\in D$. Let $(i\mapsto t)$ be the term under $\gamma$, written with $i$, $D$, $C$ and $t$, $i$ bound in it, whose value under each assignment satisfying $\gamma$ is that map $h$. Then $(i\mapsto t)$ is a term of type $C^{D}$ under $\gamma$.