fixpoint-theory-nov24/sections/background.tex

\definitionBody{powerset}{Given a set $S$, we denote its powerset, i.e.\ $\{ x \subseteq S \}$ with $\powerset(S)$. We use $\powersetO(S)$ to denote the powerset of $S$ without the empty set.}
\definitionBody{poset}{
    We call $\langle S, \lte \rangle$ a {\em poset} (a partially ordered set) if $\lte$ is reflexive, transitive and antisymmetric. 
}
\definitionBody{lubglb}{An element is an {\em upper or lower bound} of a subset $S$ of a \Poset if it is greater than or equal or less than or equal, respectively, to every element inside $S$.}
\definitionBody{completelattice}{A {\em complete lattice} is a \Poset $\langle \LL, \lte \rangle$ s.t.\ every subset $S$ of $\LL$ has a unique greatest lower bound $\glb^{\LL} S$ and least upper bound $\lub^{\LL} S$}
\definitionBody{topbot}{We use $\top^{\LL}$ and $\bot^{\LL}$ to denote $\lub^{\LL} \LL$ and $\glb^{\LL} \LL$ respectively.}
\definitionBody{monotone}{A function $f: A \rightarrow B$ is {\em monotone} w.r.t. the orderings $\langle A, \lteSub{A} \rangle$ and $\langle B, \lteSub{B} \rangle$ if for all $a_1, a_2 \in A$, $a_1 \lte a_2$ implies $f(a_1) \lte f(a_2)$}
\definitionBody{image}{Given a function $f: A \rightarrow B$, we use $f[A]$ to denote the {\em image of $f$} w.r.t.\ $A$, i.e.\ the set $\{ f(a) ~|~ a \in A \} \subseteq B$.
With abuse to notation, when given a set of functions $F$, we write $\bigcup \{ f\image{A} ~|~ f \in F \}$ as $F\image{A}$.}