$w$-Invexity and Optimality Problem

Musavvir Alia,∗ and Ehtesham Akhterb

${}^{a,~{}b}$ Department of Mathematics,
Aligarh Muslim University, Aligarh-202002, India

111∗Corresponding author
E-mail addresses<EMAIL_ADDRESS>(M. Ali),
<EMAIL_ADDRESS>(E. Akhter).

###### Abstract

##  1 Introduction

Numerous parts of mathematical programming, such as the adequate optimality
condition and the duality theorem, deeply rely on convexity. One of the
generalised convex functions is an invex function, which was first defined by
Hanson [Hanson]. Numerous generalisations of this idea have been offered in
the literature. Invex functions were transformed into
$\rho-(\eta,\theta)$-invex functions by Zalmai [20]. Semistrictly preinvex
functions on $\mathbb{R}^{n}$ were first developed by Yang and Li [17]. In
addition to expanding several findings on convexity and optimization developed
for linear spaces leading to Riemannian manifolds, Rapcsak [11] also obtained
a generalisation known as geodesic convexity. In Riemannian spaces, the
problem of convex programming with duality conditions was established by
Udriste [14] Pini [8] introduced the idea of invex functions there. A vector
programming problem described on a differentiable manifold admitting the
necessary and sufficient conditions of KKT(Karush-Kuhn-Tucker) type by
Mititelu [7]. Ferrara and Mititelu proposed the Mond-Weir form of duality for
vector programming issues on differentiable manifolds [4].

On convex-like functions, the alternative theorem and the assumption for the
semi-preinvex function as a convex-like function together used to develop
Fritz-John condition for ICOP (inequality constrained optimization problem,
[6] ). Fritz-John condition is also introduced as an example of the pre-
variational inequality problem and duality. Following Hanson and Mond [5] and
Rueda and Hanson [12], who established the relationships between the K.T.
point of a function of Type I and Type II and at least one limited
mathematical programming issue (see ([5],[12]). The link between $w$-invexity
and some proven generalizations of convexity will be covered in this study.
The introduction to generalized convexity and related subjects are covered in
Section 2. It is demonstrated that there is a fairly natural process to follow
for $w$-quasi-preinvexity, $w$-strictly quasi-invexity, and $w$-semi-strictly
quasi-invexity of the real functions in section 3, where $w$-preinvex,
$w$-quasi preinvex, $w$-strictly quasi invex, and $w$-semi-strictly quasi
preinvex functions will be discussed. We have also shown that $w$-preinvex
functions provide desired outcomes, and it follows that $w$-preinvex functions
can be transformed easily to become regular invex functions.

##  2 Preliminaries

######  Definition 2.1.

([16]-[15]) A non empty subset $X$ of $\mathbb{R}^{n}$ is known as invex if
$\exists$ a function
$\eta:\mathbb{R}^{n}\times\mathbb{R}^{n}\rightarrow\mathbb{R}^{n}$ such that
$\forall$ $z_{1},z_{2}\in X$, $\forall$ $\delta\in[0,1]$, we obtain
$z_{2}+\delta\eta(z_{1},z_{2})\in X$.

######  Definition 2.2.

([16]-[15]) A non empty subset $X$ of $\mathbb{R}^{n}$. A function
$h:X\rightarrow\mathbb{R}$ is known as preinvex if $\exists$
$\eta:\mathbb{R}^{n}\times\mathbb{R}^{n}\rightarrow\mathbb{R}^{n}$, a
function, such that $\forall$ $z_{1},z_{2}\in X$, $\forall$
$\delta\in[0,1]$,we obtain

$h(z_{2}+\delta\eta(z_{1},z_{2}))\leq\delta h(z_{1})+(1-\delta)h(z_{2}).$

######  Definition 2.3.

[9] A non empty subset $X$ of $\mathbb{R}^{n}$. A function
$h:X\rightarrow\mathbb{R}$ is known as prequasi invex if $\exists$
$\eta:\mathbb{R}^{n}\times\mathbb{R}^{n}\rightarrow\mathbb{R}^{n}$, a
function, s.t., $\forall$ $z_{1},z_{2}\in X$, $\forall$ $\delta\in[0,1]$,we
obtain

$h(z_{2}+\delta\eta(z_{1},z_{2}))\leq\max\\{h(z_{1}),h(z_{2})\\}.$

######  Definition 2.4.

[18] A non empty subset $X$ of $\mathbb{R}^{n}$. A function
$h:X\rightarrow\mathbb{R}$ is known as strictly prequasi invex if $\exists$ a
function $\eta:\mathbb{R}^{n}\times\mathbb{R}^{n}\rightarrow\mathbb{R}^{n}$
such that $\forall$ $z_{1},z_{2}\in X$ $z_{1}\neq z_{2},$ $\forall$
$\delta\in(0,1)$,we obtain

$h(z_{2}+\delta\eta(z_{1},z_{2}))<\max\\{h(z_{1}),h(z_{2})\\}.$

######  Definition 2.5.

[18] A non empty subset $X$ of $\mathbb{R}^{n}$. A function
$h:X\rightarrow\mathbb{R}$ is known as semi-strictly prequasi invex if
$\exists$ a function
$\eta:\mathbb{R}^{n}\times\mathbb{R}^{n}\rightarrow\mathbb{R}^{n}$ such that
$\forall$ $z_{1},z_{2}\in X$ $h(z_{1})\neq h(z_{2}),$ $\forall$
$\delta\in(0,1)$, we obtain

$h(z_{2}+\delta\eta(z_{1},z_{2}))<\max\\{h(z_{1}),h(z_{2})\\}.$

##  3 $w$-invexity

######  Definition 3.1.

A non-empty subset $X$ of $\mathbb{R}^{n}$ is said to be $w$-invex if there
exists map $\eta:\mathbb{R}^{n}\times\mathbb{R}^{n}\rightarrow\mathbb{R}^{n}$
and $w:\mathbb{R}^{n}\rightarrow\mathbb{R}^{n}$ such that

$w(z_{2})+\delta\eta(z_{1},w(z_{2}))\in X,~{}~{}\forall z_{1},z_{2}\in
X~{}~{}\mbox{and}~{}~{}\delta\in[0,1].$

######  Remark 3.1.

Every invex set is $w$-invex (as take $w$ is an identity map) however converse
isnﬂt always true.

######  Example 3.2.

Let $\eta:[0,\infty)\times[0,\infty)\rightarrow R$ be given by:

$\eta(z_{1},z_{2})=z_{1}(z_{2}-2),$

and let the function $w:[0,\infty)\rightarrow R$ be given by:

$w(z_{2})=z_{2}+2.$

Then $X$ is not a invex set w.r. to map $\eta$ but it is $w$-invex set w.r.to
the maps $\eta$ and $w$.

######  Definition 3.3.

Let $X$ be a $w$-invex set. A function $h:X\rightarrow\mathbb{R}$ is said to
be

(i) $w$-preinvex if $\forall$ points $z_{1},z_{2}\in X$, and $0\leq\delta\leq
1$, such that

$h(w(z_{2})+\delta\eta(z_{1},w(z_{2})))\leq\delta
h(z_{1})+(1-\delta)h(z_{2}).$

(ii) $w$-strictly preinvex if $\forall$ points $z_{1},z_{2}\in X$, $z_{1}\neq
z_{2}$ and $0<\delta<1$, such that

$h(w(z_{2})+\delta\eta(z_{1},w(z_{2})))<\delta h(z_{1})+(1-\delta)h(z_{2}).$

(iii) $w$-prequasi-invex if $\forall$ points $z_{1},z_{2}\in X$, and
$0\leq\delta\leq 1$, such that

$h(w(z_{2})+\delta\eta(z_{1},w(z_{2})))\leq\mbox{max}\\{h(z_{1}),h(z_{2})\\}.$

(iv) $w$-strictly prequasi-invex if $\forall$ points $z_{1},z_{2}\in X$,
$z_{1}\neq z_{2}$ and $0<\delta<1$, such that

$h(w(z_{2})+\delta\eta(z_{1},w(z_{2})))<\mbox{max}\\{h(z_{1}),h(z_{2})\\}.$

(v) $w$-semi-strictly prequasi-invex if $\forall$ points $z_{1},z_{2}\in X$,
$h(z_{1})\neq h(z_{2})$ and $0<\delta<1$, such that

$h(w(z_{2})+\delta\eta(z_{1},w(z_{2})))<\mbox{max}\\{h(z_{1}),h(z_{2})\\}.$

######  Remark 3.2.

In general, every $w$-strictly preinvex function is a also $w$-preinvex
function, however converse isnﬂt always true. e.g., (3.7).

######  Remark 3.3.

In general, every $w$-preinvex function is a also $w$-pre quasi-preinvex
function, however converse isnﬂt always true. e.g., (3.6).

######  Remark 3.4.

In general, every preinvex function is a also $w$-preinvex function (as take
$w$ is an identity map), however converse isnﬂt always true. e.g.,(3.7).

######  Example 3.4.

Consider $h:\mathbb{R}\rightarrow\mathbb{R},$ be defined as:
$h(z_{1})=z_{1}+k,$ where $k$ is a constant.

Let the function $w:\mathbb{R}\rightarrow\mathbb{R}$ be defined as:
$w(z_{2})=z_{2}-7,$ and consider
$\eta:\mathbb{R}\times\mathbb{R}\rightarrow\mathbb{R}$ as :
$\eta(z_{1},z_{2})=z_{1}-z_{2}-6$ for all $z_{1},z_{2}\in\mathbb{R}$. Then the
function $h$ is $w$-preinvex function w.r.to $\eta$ and $w$.

######  Example 3.5.

Consider $h:\mathbb{R}\rightarrow\mathbb{R},$ be defined as:
$h(z_{1})=z_{1}+k,$ where $k$ is a constant.

Consider the function $w:\mathbb{R}\rightarrow\mathbb{R}$ be defined as:
$w(z_{2})=z_{2}+6,$ and consider
$\eta:\mathbb{R}\times\mathbb{R}\rightarrow\mathbb{R}$ be defined as :
$\eta(z_{1},z_{2})=z_{1}-z_{2}+6$ for all $z_{1},z_{2}\in\mathbb{R}$. Then the
function $h$ is $w$-preinvex function w.r.to $\eta$ and $w$, but not
$w$-strictly preinvex and preinvex function.

######  Example 3.6.

Consider $h:\mathbb{R}\rightarrow\mathbb{R},$ be defined as:
$h(z_{1})=z_{1}^{5}$. Consider the function
$w:\mathbb{R}\rightarrow\mathbb{R}$ be defined as: $w(z_{2})=z_{2}-6,$ and
consider $\eta:\mathbb{R}\times\mathbb{R}\rightarrow\mathbb{R}$ be defined as
: $\eta(z_{1},z_{2})=z_{1}-z_{2}-6$ for all $z_{1},z_{2}\in\mathbb{R}$. Then
the function $h$ is $w$-prequasi preinvex function w.r.to $\eta$ and $w$, but
not $w$-preinvex function.

######  Example 3.7.

Let $h:\mathbb{R}\rightarrow\mathbb{R},$ be defined as: $h(z_{1})=z_{1}+k,$
where $k$ is a constant.

let the function $w:\mathbb{R}\rightarrow\mathbb{R}$ be defined as:
$w(z_{2})=z_{2}+6,$ and consider
$\eta:\mathbb{R}\times\mathbb{R}\rightarrow\mathbb{R}$ be defined as :
$\eta(z_{1},z_{2})=z_{1}-z_{2}+6$ for all $z_{1},z_{2}\in\mathbb{R}$. It is
simple to demonstrate that while $h$ is $w$-preinvex w.r.to $\eta$ and $w$
and, it is not preinvex w.r.to $\eta$.

######  Example 3.8.

Let $h:[0,\infty)\rightarrow\mathbb{R},$ be defined as:
$h(z_{1})=\begin{cases}11,\text{ if }z_{1}\in[0,11)\\\ -11,\text{ if
}z_{1}\in[11,\infty)\end{cases},$ let the function
$w:[0,\infty)\rightarrow\mathbb{R}$ be defined as: $w(z_{2})=z_{2}+11,$ and
consider $\eta:[0,\infty)\times[0,\infty)\rightarrow\mathbb{R}$ be defined as
: $\eta(z_{1},z_{2})=z_{1}^{2}+z^{2}_{2}+11$ for all
$z_{1},z_{2}\in[0,\infty)$. Then the function $h$ is $w$-pre quasi-invex
function w.r.to $\eta$ and $w$.

######  Theorem 3.9.

$h:X\rightarrow\mathbb{R}$ is $w$-preinvex function w.r.to $\eta$ and $w$ if
and only if the epigraph of $h$,

$epi(h)=\\{(z,\alpha):\alpha\in\mathbb{R},h(z)\leq\alpha\\},$

is $w$-invex w.r.to the same $\eta$ and $w$, where $X$ is any non-empty
$w$-invex subset of $\mathbb{R}^{n}$.

###### Proof.

Consider $h:X\rightarrow\mathbb{R}$ be a $w$-preinvex function w.r.to $\eta$
and $w$. Suppose that $(z_{1},\alpha)$ and $(z_{2},\beta)\in epi(h)$, with
$z_{1},z_{2}\in X$, $h(z_{1})\leq\alpha$ and $h(z_{2})\leq\beta$, for
$\alpha,\beta\in\mathbb{R}$. Thus,

$\displaystyle h(w(z_{2})+\delta\eta(z_{1},w(z_{2})))$ $\displaystyle\leq$
$\displaystyle\delta h(z_{1})+(1-\delta)h(z_{2}).$ $\displaystyle=$
$\displaystyle\delta\alpha+(1-\delta)\beta,~{}~{}\mbox{for}~{}\delta\in[0,1]$

which implies that

$(w(z_{2})+\delta\eta(z_{1},w(z_{2})),~{}\delta\alpha+(1-\delta)\beta)\in
epi(h),$

showing that $epi(h)$ is $w$-invex w.r.to the maps $\eta$ and $w$. Conversely,
assume that $epi(h)$ is $w$-invex set w.r.to the maps $\eta$ and $w$. Take
$z_{1},z_{2}\in X$. Then $(z_{1},h(z_{1})),(z_{2},h(z_{2}))\in epi(h)$, it
follows that

$(w(z_{2})+\delta\eta(z_{1},w(z_{2})),~{}\delta
h(z_{1})+(1-\delta)h(z_{2}))\in epi(h),~{}~{}\forall\delta\in[0,1]$

$\implies$

$h(w(z_{2})+\delta\eta(z_{1},w(z_{2})))\leq\delta
h(z_{1})+(1-\delta)h(z_{2}).$

By doing so, it is demonstrated that h is a w-preinvex function w.r.to the map
$\eta$ and $w$. Completeness of the proof.

∎

######  Theorem 3.10.

Consider $h:X\rightarrow\mathbb{R}$ be a $w$-preinvex function w.r.to the
functions $\eta$ and $w$, where $X$ is any non-empty $w$-invex subset of
$R^{n}$. Then, the level set

$M_{\alpha}=\\{z\in X,h(z)\leq\alpha,\alpha\in\mathbb{R}\\}$

is $w$-invex w.r.to the same map $\eta$ and $w$.

###### Proof.

Let $z_{1},z_{2}\in M_{\alpha}$. Then $z_{1},z_{2}\in X$ and
$h(z_{1})\leq\alpha,h(z_{2})\leq\alpha$. Since $h$ is $w$-preinvex then, we
have, $\forall\in[0,1]$,

$\displaystyle h(w(z_{2})+\delta\eta(z_{1},w(z_{2})))$ $\displaystyle\leq$
$\displaystyle\delta h(z_{1})+(1-\delta)h(z_{2}).$ $\displaystyle=$
$\displaystyle\delta\alpha+(1-\delta)\alpha,~{}~{}\mbox{for}~{}\delta\in[0,1]$
$\displaystyle=$ $\displaystyle\alpha.$

This shows that $w(z_{2})+\delta\eta(z_{1},w(z_{2}))\in X$, and the level set
$M_{\alpha}$ is a $w$-invex set w.r.to the map $\eta$ and $w$. ∎

######  Theorem 3.11.

The function $h:X\rightarrow\mathbb{R}$ is $w$-quasi preinvex w.r.to the same
$\eta$ and $w$ $\iff$ the level set

$M_{\alpha}=\\{z\in X,h(z)\leq\alpha,\alpha\in\mathbb{R}\\}$

is $w$-invex w.r.to the same $\eta$ and $w$, where $X$ is any non-empty
$w$-invex subset of $R^{n}$.

###### Proof.

Suppose that the function $h$ is $w$-quasi preinvex w.r.to the maps $\eta$ and
$w$. Let $z_{1},z_{2}\in M_{\alpha}.$ Then, $z_{1},z_{2}\in X$ and
$\mbox{max}\\{h(z_{1}),h(z_{2})\\}\leq\alpha$. Since $X$ is a $w$-invex set,
so, $\forall~{}\delta\in[0,1],$

$(w(z_{2})+\delta\eta(z_{1},w(z_{2}))\in X.$

Since $h$ is $w$-quasi preinvex function, we have

$h(w(z_{2})+\delta\eta(z_{1},w(z_{2})))\leq\mbox{max}\\{h(z_{1}),h(z_{2})\\}\leq\alpha,$

$\implies$

$(w(z_{2})+\delta\eta(z_{1},w(z_{2}))\in M_{\alpha}.$

This implies that $M_{\alpha}$ is a $w$-invex set w.r.to the maps $\eta$ and
$w$.

Conversely assume that the level set $M_{\alpha}$ is $w$-invex w.r.to the maps
$\eta$ and $w$. Let $z_{1},z_{2}\in M_{\alpha}$ for
$\mbox{max}\\{h(z_{1}),h(z_{2})\\}=\alpha.$ Since $X$ is a $w$-invex set, we
have

$w(z_{2})+\delta\eta(z_{1},w(z_{2}))\in X,$

implies that

$h(w(z_{2})+\delta\eta(z_{1},w(z_{2})))\leq\mbox{max}\\{h(z_{1}),h(z_{2})\\}=\alpha.$

This prove that $h$ is a $w$-quasi preinvex function w.r.to the functions
$\eta$ and $w$. ∎

######  Theorem 3.12.

Assume that $h:X\rightarrow\mathbb{R}$ is a $w$-preinvex function w.r.to the
maps $\eta$ and $w$, where $X$ is any non-empty $w$-invex subset of $R^{n}$
and $\nu=inf_{z\in X}h(z).$ Then, the set

$F=\\{z\in X:h(z)=\nu\\}$

is $w$-invex w.r.to the same $\eta$ and $w$. If $h$ is $w$-strictly preinvex
then $F$ is a singleton.

###### Proof.

Assume that $z_{1},z_{2}\in X$ and $\delta\in[0,1]$. Since $h$ is a
$w$-preinvex then, we have

$\displaystyle h(w(z_{2})+\delta\eta(z_{1},w(z_{2})))$ $\displaystyle\leq$
$\displaystyle\delta h(z_{1})+(1-\delta)h(z_{2})$ $\displaystyle=$
$\displaystyle\delta\nu+(1-\delta)\nu,~{}~{}\mbox{for}~{}\delta\in[0,1]$
$\displaystyle=$ $\displaystyle\nu.$

This follows that

$w(z_{2})+\delta\eta(z_{1},w(z_{2}))\in F,$

which implies that $F$ is $w$-invex w.r.to the maps $\eta$ and $w$.
For the other part, contrarily suppose that $h(z_{1})=h(z_{2})=\nu$. Since $X$
is a $w$-invex set, so

$w(z_{2})+\delta\eta(z_{1},w(z_{2}))\in F,~{}~{}\forall~{}~{}\delta\in[0,1].$

Also, since $h$ is $w$-strictly preinvex, we have

$\displaystyle h(w(z_{2})+\delta\eta(z_{1},w(z_{2})))$ $\displaystyle<$
$\displaystyle\delta h(z_{1})+(1-\delta)h(z_{2})$ $\displaystyle=$
$\displaystyle\delta\nu+(1-\delta)\nu,~{}~{}\mbox{for}~{}\delta\in[0,1]$
$\displaystyle=$ $\displaystyle\nu.$

This contradiction the fact that $\nu=inf_{z\in X}h(z).$ Therefore, $F$ is
singleton. ∎

######  Theorem 3.13.

Let $h:X\rightarrow\mathbb{R}$ is a $w$-preinvex function on $X$, where $X$ is
any non-empty $w$-invex subset of $R^{n}$. Therefore, any local minimum point
is also a global minimum point.

###### Proof.

Assuming that $z_{2}\in X$ is not a global minimum point, let $z_{2}$ be the
local minimum point for $h$. Then, $\exists$ $z_{1}\in X$ such that,
$h(z_{1})\leq h(z_{2})$. Since $h$ is $w$-preinvex $X$, $\exists$ $\eta$ and
$w$ such that, $\forall$ $\delta\in[0,1]$, we have

$\displaystyle h(w(z_{2})+\delta\eta(z_{1},w(z_{2})))$ $\displaystyle\leq$
$\displaystyle\delta h(z_{1})+(1-\delta)h(z_{2})$ (3.1) $\displaystyle<$
$\displaystyle\delta h(z_{2})+(1-\delta)h(z_{2})$ $\displaystyle=$
$\displaystyle h(z_{2}).$

Given that $z_{2}$ represents a global minimum then $\exists$ a neighbourhood
$N$ of $z_{2}$ such that
$h(z)\geq h(z_{2})$, $\forall$ $z\in N\cap X$. As
$w(z_{2})+\delta\eta(z_{1},w(z_{2}))\in X$ for each $\delta\in[0,1]$,
$\exists$ $\epsilon>0$ such that $w(z_{2})+\delta\eta(z_{1},w(z_{2}))\in X\cap
N$ for each $\delta\in[0,\epsilon)$, in a contradiction with 3.1. ∎

######  Theorem 3.14.

Let $h:X\rightarrow\mathbb{R}$ is a $w$-preinvex function on $X$, where $X$ is
any non-empty $w$-invex subset of $R^{n}$. Any strict local minimum point is
thus a strict global minimum point.

###### Proof.

The proof is same lines as of Theorem 3.13. ∎

######  Theorem 3.15.

If $h:X\rightarrow\mathbb{R}$ is $w$-preinvex on the $w$-invex set $X$, where
$X$ is any non-empty $w$-invex subset of $R^{n}$, then also $kh$ is
$w$-preinvex w.r.to $\eta$ and $w$, for any $k>0$.

###### Proof.

Since $h$ is a $w$-preinvex function then, we have $\forall$ $z_{1},z_{2}\in
X$ and $\delta\in[0,1]$

$h(w(z_{2})+\delta\eta(z_{1},w(z_{2})))\leq\delta
h(z_{1})+(1-\delta)h(z_{2}),$

we have, for any $k>0$,

$k(h(w(z_{2})+\delta\eta(z_{1},w(z_{2}))))\leq k(\delta
h(z_{1})+(1-\delta)h(z_{2})),~{}~{}\forall\delta\in[0,1]$

from which

$k(h(w(z_{2})+\delta\eta(z_{1},w(z_{2}))))\leq\delta(kh)(z_{1})+(1-\delta)(kh)(z_{2}),~{}~{}\forall\delta\in[0,1].$

∎

######  Theorem 3.16.

Let $h_{1},h_{2}:X\rightarrow\mathbb{R}$ be two $w$-preinvex functions w.r.to
the same functions $\eta$ and $w$, where $X$ is any non-empty $w$-invex subset
of $R^{n}$. Then, $h_{1}+h_{2}$ is a $w$-preinvex function w.r.to same $\eta$
and $w$.

###### Proof.

Because $h_{1}$ and $h_{2}$ are $w$-preinvex w.r.to $\eta$ and $w$, we have

$h_{1}(w(z_{2})+\delta\eta(z_{1},w(z_{2})))\leq\delta
h_{1}(z_{1})+(1-\delta)h_{1}(z_{2}).$

And

$h_{2}(w(z_{2})+\delta\eta(z_{1},w(z_{2})))\leq\delta
h_{2}(z_{1})+(1-\delta)h_{2}(z_{2}).$

By combining the aforementioned relationships, we get

$(h_{1}+h_{2})(w(z_{2})+\delta\eta(z_{1},w(z_{2})))\leq\delta(h_{1}+h_{2})(z_{1})+(1-\delta)(h_{1}+h_{2})(z_{2}).$

∎

Theorems 3.15 and 3.16 have a direct impact on the following.

######  Theorem 3.17.

Let $h_{i}:X\rightarrow\mathbb{R}$, $i=1,2,...,m,$ be $w$-preinvex w.r.to same
$\eta$ and $w$, where $X$ is any non-empty $w$-invex subset of $R^{n}$. Then
$\sum_{i=1}^{m}k_{i}h_{i}(z)$ is $w$-preinvex w.r.to same $\eta$ and $w$,
where $k_{i}>0$, $i=1,2,...,m.$

######  Theorem 3.18.

Let $h:X\rightarrow\mathbb{R}$ be a $w$-preinvex w.r.to $\eta$ and $w$, where
$X$ is any non-empty $w$-invex subset of $R^{n}$, let
$\phi:\mathbb{R}\rightarrow\mathbb{R}$ be an increasing and convex. Then
$\phi\circ h$ is $w$-preinvex w.r.to $\eta$ and $w$.

###### Proof.

As $h$ is $w$-preinvex w.r.to $\eta$ and $w$, we obtain $\forall$
$z_{1},z_{2}\in X,\delta\in[0,1]$,

$h(w(z_{2})+\delta\eta(z_{1},w(z_{2})))\leq\delta
h(z_{1})+(1-\delta)h(z_{2}).$

Due to the fact that $\phi:\mathbb{R}\rightarrow\mathbb{R}$ non-decreasing and
convex, we obtain

$\displaystyle\phi(h(w(z_{2})+\delta\eta(z_{1},w(z_{2}))))$
$\displaystyle\leq$ $\displaystyle\phi(\delta(h(z_{1})+(1-\delta)h(z_{2}))$
$\displaystyle\leq$
$\displaystyle\delta\phi(h(z_{1}))+(1-\delta)\phi(h(z_{1})),$

or

$\phi\circ h(w(z_{2})+\delta\eta(z_{1},w(z_{2}))\leq\delta\phi\circ
h(z_{1})+(1-\delta)\phi\circ h(z_{1})$

∎

######  Definition 3.19.

Let $X$ is any non-empty $w$-invex subset of $R^{n}$.
$h:X\rightarrow\mathbb{R}$ is said to be $w$-pre pseudo-invex function if
$\exists$ functions $\eta$, $w$ and a function $b$, positve on domain, such
that

$h(z_{1})<h(z_{2})\implies h(z_{2}+\delta\eta(z_{1},w(z_{2})))\leq
h(z_{2})+\delta(\delta-1)b(z_{1},z_{2})$

for every $\delta\in(0,1)$ and $z_{1},z_{2}\in X$.

######  Theorem 3.20.

If $h$ is $w$-preinvex, then $h$ is $w$-pre pseudo-invex w.r.to the same
$\eta$ and $w$, where $X$ is any non-empty $w$-invex subset of $R^{n}$.

###### Proof.

For $h(z_{1})<h(z_{2})$, for every $\delta\in(0,1),$ we can write

$\displaystyle(h(w(z_{2})+\delta\eta(z_{1},w(z_{2}))))$ $\displaystyle\leq$
$\displaystyle h(z_{2})+\delta[h(z_{1})-h(z_{2})]$ $\displaystyle<$
$\displaystyle
h(z_{2})+\delta[h(z_{1})-h(z_{2})]-\delta^{2}[h(z_{1})-h(z_{2})],$
$\displaystyle=$ $\displaystyle h(z_{2})+\delta(\delta-1)[h(z_{2})-h(z_{1})],$

where $b(z_{1},z_{2})=h(z_{2})-h(z_{1})>0.$ ∎

######  Theorem 3.21.

Let $h:X\rightarrow\mathbb{R}$ is a $w$-pre pseudo-invex function, where $X$
is any non-empty $w$-invex subset of $R^{n}$. Consequently, any local minimum
point is also a global minimum point.

###### Proof.

Let us assume irrationally that $z_{2}$ be local minimum point rather than a
global one. Then $\exists$ $z_{1}\in X$ such that $h(z_{1})<h(z_{2}).$
According to the $w$-pre pseudo-invexity definition, which means that, we have
$\exists$ $b(z_{1},z_{2})>0$, such that, $\forall$ $\delta\in(0,1)$,

$h(z_{2}+\delta\eta(z_{1},w(z_{2})))\leq
h(z_{2})+\delta(\delta-1)b(z_{1},z_{2})<h(z_{2}),$

from which $h(z_{2})>h(w(z_{2})+\delta\eta(z_{1},w(z_{2})))$, $\forall$
$\in(0,1),$
in contradiction with the assumption. ∎

######  Theorem 3.22.

Assume that $\eta(z_{1},w(z_{2}))\neq 0$ whenever $z_{1}\neq w(z_{2})$. Let
$h$ be a $w$-pre quasi-invex function on $X$ w.r.to $\eta$ and $w$, where $X$
is any non-empty $w$-invex subset of $R^{n}$. Consequently, any strict local
minimum point is $h$ also a strict global minimum point.

###### Proof.

Contrarily suppose that $z_{2}$ be strict local minimum but not global; then
$\exists$ $z\in X$ s.t., $h(z)<h(z_{2}).$ Since $h$ is $w$-pre quasi-invex, we
have

$h(z_{2}+\delta\eta(z,w(z_{2})))\leq h(z_{2}),$

a contradiction. ∎

######  Theorem 3.23.

Let $h:X\rightarrow\mathbb{R}$ be a $w$-pre quasi-invex function w.r.to
$\eta$, where $X$ is any non-empty $w$-invex subset of $R^{n}$ and $w$.
Suppose that $\phi:\mathbb{R}\rightarrow\mathbb{R}$ is a increasing function,
then, $\phi\circ h$ is $w$-pre quasi-invex w.r.to $\eta$ and $w$.

###### Proof.

Given that $h$ is $w$-pre quasi-invex function and $\phi$ is a increasing, we
obtain

$\phi\circ
h(w(z_{2})+\delta\eta(z_{1},w(z_{2})))\leq\phi(\mbox{max}\\{h(z_{1}),h(z_{2})\\}).$
$\displaystyle\phi\circ h(w(z_{2})+\delta\eta(z_{1},w(z_{2})))$
$\displaystyle\leq$ $\displaystyle\phi(\mbox{max}\\{h(z_{1}),h(z_{2})\\})$
$\displaystyle=$ $\displaystyle\mbox{max}\\{\phi\circ h(z_{1}),\phi\circ
h(z_{2})\\},$

which expresses the fact that the composition function $\phi\circ h$ is
$w$-pre quasi-invex.

∎

##  4 Optimality

Let $h:\mathbb{R}^{n}\rightarrow\mathbb{R}$ and
$g_{i}:\mathbb{R}^{n}\rightarrow\mathbb{R}$, $i=1,2,....,m$ are $w$-preinvex
functions on $\mathbb{R}^{n}$. A $w$-preinvex programming problem is
formulated as follows:

Min h(z) (4.1) subject to $\displaystyle\text{z}\in
X=\\{z\in\mathbb{R}^{n}:g_{i}(z)\leq 0,\;i=1,\ldots,m\\}.$

######  Theorem 4.1.

If $h:\mathbb{R}^{n}\rightarrow\mathbb{R}$ is $w$-strictly preinvex function
on $X$, where $X$ is any non-empty $w$-invex subset of $R^{n}$, then the
global optimal solution of problem (4.1) is unique.

###### Proof.

Let $z_{1},z_{2}\in X$ be different global optimal solution of problem (4.1).
Then $h(z_{1})=h(z_{2})$. Since $h$ is $w$-strictly invex then, we have

$\displaystyle h(w(z_{2})+\delta\eta(z_{1},w(z_{2})))$ $\displaystyle<$
$\displaystyle\delta h(z_{1})+(1-\delta)h(z_{2})$ $\displaystyle=$
$\displaystyle h(z_{1}),$
$h(w(z_{2})+\delta\eta(z_{1},w(z_{2})))<h(z_{1}),~{}~{}for~{}~{}each~{}~{}\delta\in(0,1).$

This contradicts the optimality of $z_{2}$ for problem(4.1). Hence, the global
optimal solution of problem (4.1) is unique. ∎

######  Theorem 4.2.

Let $h:\mathbb{R}^{n}\rightarrow\mathbb{R}$ be $w$-quasi preinvex function on
$X$, where $X$ is any non-empty $w$-invex subset of $R^{n}$ and let
$\gamma=\min_{z\in X}h(z)$. The set $X=\\{z\in X:h(z)=\gamma\\}$ of optimal
solution of problem (4.1) is $w$-invex set.
If $h$ is $w$-strictly quasi-invex, then the set $X$ is a singleton.

###### Proof.

Let $z_{1},z_{2}\in X$ be different global optimal solution of problem (4.1).
Then

$h(z_{1})=h(z_{2})=\gamma.$

Since $h:\mathbb{R}^{n}\rightarrow\mathbb{R}$ be $w$-quasi preinvex function
on $X$, then

$h(w(z_{2})+\delta\eta(z_{1},w(z_{2})))\leq\mbox{max}\\{h(z_{1}),h(z_{2})\\}=\gamma$

which implies that $h(w(z_{2})+\delta\eta(z_{1},w(z_{2}))\in X,$ so $X$ is
$w$-invex set.
For the other part, on contrary let $z_{1},z_{2}\in X$, $z_{1}\neq
z_{2},~{}~{}\delta\in(0,1),$ then $h(w(z_{2})+\delta\eta(z_{1},w(z_{2}))\in
X.$
Further, since $h$ is $w$-strictly quasi preinvexity function on $X$, we have

$h(w(z_{2})+\delta\eta(z_{1},w(z_{2})))\leq\mbox{max}\\{h(z_{1}),h(z_{2})\\}=\gamma.$

This contradicts that $\gamma=\min_{z\in X}h(z)$ and hence the results
follows. ∎

######  Theorem 4.3.

Consider the function $h:\mathbb{R}^{n}\rightarrow\mathbb{R}$ is $w$-pre
quasi-preinvex on a $w$-invex subset of $\mathbb{R}^{n}$. Suppose
$\gamma=\min_{z\in X}h(z)$. Then the optimal solutions of problem (4.1) i.e.,
$Y=\\{z\in X\ :h(z)=\gamma\\}$ is a $w$-invex set. If $h$ is $w$-strictly
quasi-preinvex on a $w$-invex subset of $\mathbb{R}^{n}$. Then $w$-invex set a
singleton set.

###### Proof.

Let $z_{1},z_{2}\in Y$ and $\delta\in[0,1]$, then $z_{1},z_{2}\in X$ also
$h(z_{1})=\gamma$, $h(z_{2})=\gamma$. As $h$ is $w$-pre quasi preinvex
function on $w$-invex set, we have

$w(z_{2})+\delta\eta(z_{2},w(z_{1}))\in X$

and

$h(w(z_{2})+\delta\eta(z_{2},w(z_{1})))\leq\max\\{h(z_{1}),h(z_{2})\\}=\gamma$

which shows that

$(w(z_{2})+\delta\eta(z_{2},w(z_{1}))\in Y,$

it demonstrate that $X$-invex set.
For the other part, suppose to the contrary that $z_{1},z_{2}\in X$, and
$z_{1}\neq z_{2}$, $\delta\in(0,1)$, we get

$w(z_{2})+\delta\eta(z_{2},w(z_{1}))\in X$

As $h$ is $w$-strictly quasi preinvex on $X$, we get

$h(w(z_{2})+\delta\eta(z_{2},w(z_{1})))<\max\\{h(z_{1}),h(z_{2})\\}=\gamma,$

there is a contradiction. ∎

## References

  * [1] Caristi, G., Ferrara, M. and Stefanescu, A., 2010. Semi-infinite multiobjective programming with generalized invexity. Mathematical Reports, 62, pp.217-233.
  * [2] Das, K. and Nahak, C., 2020. Sufficiency and duality in set-valued optimization problems under $(p,r)-\rho-(\eta,\theta)$-invexity. Acta Univ. Apulensis, 62, pp.93-110.
  * [3] Edalat, G., Sadeghieh, A. and Caristi, G., 2019. Characterization of efficient solutions in nonsmooth multiobjective problems using generalized invexity. Numerical Computations: Theory and Algorithms NUMTA 2019, p.136.
  * [4] Ferrara M, Mititelu S. Mond-Weir Duality in vector programming with generalized invex functions on differentiable manifolds. Balkan Journal of Geometry and Its Applications. 2006 Jan 1;11(2):80.
  * [5] Hanson, M.A., 1981. On sufficiency of the Kuhn-Tucker conditions. Journal of Mathematical Analysis and Applications, 80(2), pp.545-550.
  * [6] Jeyakumar, V. Convexlike alternative theorems and mathematical programming. Optimization 16, no. 5 (1985): 643-652.
  * [7] 12\. Mititelu, S.: Generalized invexity and vector optimization on differentiable manifolds. Differ. Geom. Dyn. Syst. 3, 21–31 (2001)
  * [8] Pini, R., 1994. Convexity along curves and invexity. Optimization, 29(4), pp.301-309.
  * [9] Pini, R., 1991. Invexity and generalized convexity. Optimization, 22(4), pp.513-525.
  * [10] Kiliçman, A. and Saleh, W., 2018. Generalized preinvex functions and their applications. Symmetry, 10(10), p.493.
  * [11] Rapcsak, T., 1991. Geodesic convexity in nonlinear optimization. Journal of Optimization Theory and Applications, 69(1), pp.169-183.
  * [12] Rueda N. G, And Hanson M. A. Optimality criteria [or mathematical programmmg mvolving generalized invexlty, J. Math. Anal. .4ppl. 130 (1988). 375-385
  * [13] Reddy, L.V., Singh, A. and Pandey, S.P., 2019. Generalized Invexity and Semi–Continuity In Mathematical Programming. International Journal of Applied Engineering Research, 14(12), pp.2960-2967.
  * [14] Udriste, C., 2013. Convex functions and optimization methods on Riemannian manifolds (Vol. 297). Springer Science and Business Media.
  * [15] Weir T, Jeyakumar V. A class of nonconvex functions and mathematical programming. Bulletin of the Australian Mathematical Society. 1988 Oct;38(2):177-89.
  * [16] Weir, T., and Mond, B. (1988). Pre-invex functions in multiple objective optimization. Journal of Mathematical Analysis and applications, 136(1), 29-38.
  * [17] Yang, X.M. and Li, D., 2001. Semistrictly preinvex functions. Journal of Mathematical Analysis and Applications, 258(1), pp.287-308.
  * [18] Yang X.M., Yang X.Q., Teo K.L. Characterizations and applications of prequasi-invex functions. Journal of Optimization Theory and Applications. 2001 Sep;110(3):645-68.
  * [19] Zǎlinescu, C., 2014. A critical view on invexity. Journal of Optimization Theory and Applications, 162(3), pp.695-704.
  * [20] Zalmai, G.J., 1990. Generalized sufficiency criteria in continuous-time programming with application to a class of variational-type inequalities. Journal of mathematical analysis and applications, 153(2), pp.331-355.
  * [21] Rockafellar, R.T.: Convex Analysis., Princeton University Press, Princeton (1970).


a^{\prime}\mathrel{r}\left\\{b\right\\}\mathrel{\,\&\,}a^{\prime}\mathrel{r}\left\\{c\right\\}\;\rightarrow\>\exists
D\in\mathsf{Fin}(b\downarrow_{\sqsubset^{\prime}}c)\left(a\mathrel{r}D\right).$
(4.9)

######  Lemma .

An approximable map
$r\colon(S,\mathrel{\blacktriangleleft},\sqsubset)\to(S^{\prime},\mathrel{\blacktriangleleft}^{\prime},\sqsubset^{\prime})$
is Lawson approximable if and only if the corresponding approximable relation
$\mathrel{\widetilde{r}}\colon{(\mathrm{L}(S,\mathrel{\blacktriangleleft}),\mathrel{\widetilde{\ll_{\mathrel{\blacktriangleleft}}}})}\to(\mathrm{L}(S^{\prime},\mathrel{\blacktriangleleft}^{\prime}),\mathrel{\widetilde{\ll_{\mathrel{\blacktriangleleft}^{\prime}}}})$
is Lawson approximable.

###### Proof.

Suppose that $r$ is Lawson approximable, and let
$A\mathrel{\widetilde{\ll_{\mathrel{\blacktriangleleft}}}}A^{\prime}$. Then,
there exists $A^{\prime\prime}\in\mathsf{Fin}(S)$ such that
$A\mathrel{\widetilde{\mathrel{\blacktriangleleft}}}A^{\prime\prime}\sqsubset_{L}A^{\prime}$.
Since $r$ is Lawson approximable, there exists $B\in\mathsf{Fin}(S^{\prime})$
such that $A^{\prime\prime}\mathrel{\widetilde{r}}B$. Then
$A\mathrel{\mathrel{\widetilde{r}}}B$. Next, suppose
$A\mathrel{\widetilde{\ll_{\mathrel{\blacktriangleleft}}}}A^{\prime}\mathrel{\mathrel{\widetilde{r}}}B$
and $A^{\prime}\mathrel{\widetilde{r}}C$. Then, there exists
$A^{\prime\prime}\in\mathsf{Fin}(S)$ such that
$A\mathrel{\widetilde{\mathrel{\blacktriangleleft}}}A^{\prime\prime}\sqsubset_{L}A^{\prime}$.
Since $r$ is Lawson approximable, there exists $D\in\mathsf{Fin}(S^{\prime})$
such that $A^{\prime\prime}\mathrel{\widetilde{r}}D$,
$D\mathrel{\widetilde{\ll_{\mathrel{\blacktriangleleft}^{\prime}}}}B$, and
$D\mathrel{\widetilde{\ll_{\mathrel{\blacktriangleleft}^{\prime}}}}C$. Then,
$A\mathrel{\mathrel{\widetilde{r}}}D$.

Conversely, suppose that $\mathrel{\widetilde{r}}$ is Lawson approximable. If
$a\sqsubset a^{\prime}$, then
$\left\\{a\right\\}\mathrel{\widetilde{\ll_{\mathrel{\blacktriangleleft}}}}\left\\{a^{\prime}\right\\}$.
Since $\mathrel{\widetilde{r}}$ is Lawson approximable, there exists
$B\in\mathsf{Fin}(S)$ such that
$\left\\{a\right\\}\mathrel{\mathrel{\widetilde{r}}}B$, and so
$a\mathrel{r}B$. Next, suppose $a\sqsubset a^{\prime}\mathrel{r}B$ and
$a^{\prime}\mathrel{r}C$. Then,
$\left\\{a\right\\}\mathrel{\widetilde{\ll_{\mathrel{\blacktriangleleft}}}}\left\\{a^{\prime}\right\\}\mathrel{\mathrel{\widetilde{r}}}B$,
and $\left\\{a^{\prime}\right\\}\mathrel{\mathrel{\widetilde{r}}}C$. Since
$\mathrel{\widetilde{r}}$ is Lawson approximable, there exists
$D\in\mathsf{Fin}(S^{\prime})$ such that
$D\mathrel{\widetilde{\ll_{\mathrel{\blacktriangleleft}^{\prime}}}}B$,
$D\mathrel{\widetilde{\ll_{\mathrel{\blacktriangleleft}^{\prime}}}}C$, and
$\left\\{a\right\\}\mathrel{\mathrel{\widetilde{r}}}D$. Then $a\mathrel{r}D$.
∎

######  Definition .

A join-preserving Lawson approximable map between localized strong continuous
finitary covers is called a _proximity map_.

Let $\mathsf{LSContFCov}$ be the category of localized strong continuous
finitary covers and proximity maps.

######  Proposition .

The equivalence between $\mathsf{SContFCov}$ and $\mathsf{SPxJLat}$ restricts
to an equivalence between $\mathsf{LSContFCov}$ and $\mathsf{LSPxJLat}$.

###### Proof.

By Lemma 4.4 and Lemma 4.4, the embedding of $\mathsf{SContFCov}$ into
$\mathsf{SPxJLat}$ restricts to an embedding of $\mathsf{LSContFCov}$ into
$\mathsf{LSPxJLat}$. Moreover, for any localized strong proximity
$\vee$-semilattice $(S,0,\vee,\prec)$, the strong continuous finitary cover
$(S,\mathrel{\blacktriangleleft}_{\vee},\prec)$ defined in (4.3) is localized
by Lemma 3.5 and Lemma 4.4. As in Lemma 4.3, one can also show that every
isomorphism in $\mathsf{PxPos}$ is Lawson approximable. Thus, the embedding of
$\mathsf{LSContFCov}$ into $\mathsf{LSPxJLat}$ is essentially surjective. ∎

###  4.5. Formal topologies

We relate the theory of strong continuous finitary covers to that of
continuous lattices and locally compact locales in formal topology [Neg98].

######  Definition .

A _basic cover_ is a pair $(S,\mathrel{\lhd})$ where $\mathrel{\lhd}$ is a
relation between $S$ and $\mathsf{Pow}(S)$ satisfying

$\displaystyle\frac{a\in
U}{a\mathrel{\lhd}U}\;\text{(reflexivity)}\qquad\qquad\frac{a\mathrel{\lhd}U\quad
U\mathrel{\lhd}V}{a\mathrel{\lhd}V}\;\text{(transitivity)}$

where $U\mathrel{\lhd}V\stackrel{{\scriptstyle\textup{def}}}{{\iff}}\forall
a\in U\left(a\mathrel{\lhd}V\right)$. A basic cover $(S,\mathrel{\lhd})$ is
_continuous_ if it is equipped with a relation $\mathsf{wb}\subseteq S\times
S$ satisfying

$a\mathrel{\lhd}\mathsf{wb}^{-}a\qquad\qquad\frac{b\mathrel{\mathsf{wb}}a\quad
a\mathrel{\lhd}U}{\exists A\in\mathsf{Fin}(U)\;b\mathrel{\lhd}A}.$ (4.10)

Among the various definitions of formal topology described in [CMS13], we
prefer to work with the one with a preorder.

######  Definition .

A _formal topology_ is a triple $(S,\mathrel{\lhd},\leq)$ where
$(S,\mathrel{\lhd})$ is a basic cover and $(S,\leq)$ is a preorder satisfying

$\frac{a\leq
b}{a\mathrel{\lhd}\\{b\\}}\;\text{($\leq$-left)}\qquad\qquad\frac{a\mathrel{\lhd}U\quad
a\mathrel{\lhd}V}{a\mathrel{\lhd}U\downarrow_{\leq}V}\;\text{($\mathord{\downarrow}$-right)}$

where $U\downarrow_{\leq}V\stackrel{{\scriptstyle\textup{def}}}{{\ =\
}}\mathord{\downarrow}_{\leq}U\cap\mathord{\downarrow}_{\leq}V$. A formal
topology $(S,\mathrel{\lhd},\leq)$ is _locally compact_ if
$(S,\mathrel{\lhd})$ is a continuous basic cover.

A subset $U\subseteq S$ of a basic cover $(S,\mathrel{\lhd})$ is _saturated_
if

$a\mathrel{\lhd}U\;\rightarrow\>a\in U.$

Negri [Neg98] showed that the collection of saturated subsets of a continuous
basic cover and that of a locally compact formal topology are continuous
lattice and locally compact locale, respectively. She also showed that every
continuous lattice and locally compact locale can be represented in this
way.888In Negri [Neg98], continuous basic covers and locally compact formal
topologies are called _locally Stone infinitary preorders_ and _locally Stone
formal topologies_ , respectively.

######  Proposition .

Let $(S,\mathrel{\blacktriangleleft},\sqsubset)$ be a strong continuous
finitary cover. Define a relation
${\mathrel{\blacktriangleleft}_{\sqsubset}}\subseteq S\times\mathsf{Pow}(S)$
by

$a\mathrel{\mathrel{\blacktriangleleft}_{\sqsubset}}U\stackrel{{\scriptstyle\textup{def}}}{{\iff}}\forall
b\sqsubset a\,\exists
B\in\mathsf{Fin}(U)\left(b\ll_{\mathrel{\blacktriangleleft}}B\right).$ (4.11)

  1. (1)

The structure $(S,\mathrel{\blacktriangleleft}_{\sqsubset})$, is a continuous
basic cover with respect to $\sqsubset$.

  2. (2)

Let $\sqsubseteq$ be the reflexive closure of $\sqsubset$. Then,
$(S,\mathrel{\blacktriangleleft},\sqsubset)$ is localized if and only if the
triple $(S,\mathrel{\blacktriangleleft}_{\sqsubset},\sqsubseteq)$ is a locally
compact formal topology.

###### Proof.

1. This is straightforward to check.

2. Suppose that $(S,\mathrel{\blacktriangleleft},\sqsubset)$ is localized. Since ${\sqsubset\circ\sqsubseteq}\subseteq{\sqsubset}$, $(S,\mathrel{\blacktriangleleft}_{\sqsubset},\sqsubseteq)$ satisfies ($\leq$-left). As for ($\mathord{\downarrow}$-right), suppose $a\mathrel{\mathrel{\blacktriangleleft}_{\sqsubset}}U$ and $a\mathrel{\mathrel{\blacktriangleleft}_{\sqsubset}}V$. Let $b\sqsubset a$, and choose $c,d\in S$ such that $b\sqsubset c\sqsubset d\sqsubset a$. Then, there exist $A\in\mathsf{Fin}(U)$ and $B\in\mathsf{Fin}(V)$ such that $d\ll_{\mathrel{\blacktriangleleft}}A$ and $d\ll_{\mathrel{\blacktriangleleft}}B$. Thus, there exist $A^{\prime}\sqsubset_{L}A$ and $B^{\prime}\sqsubset_{L}B$ such that $d\mathrel{\blacktriangleleft}A^{\prime}$ and $d\mathrel{\blacktriangleleft}B^{\prime}$. By Lemma 4.4, there exists $C\in\mathsf{Fin}(A^{\prime}\downarrow_{\sqsubset}B^{\prime})\subseteq\mathsf{Fin}(A\downarrow_{\sqsubset}B)$ such that $c\mathrel{\blacktriangleleft}C$. Then $b\ll_{\mathrel{\blacktriangleleft}}C$, and so $a\mathrel{\mathrel{\blacktriangleleft}_{\sqsubset}}U\downarrow_{\sqsubseteq}V$. Conversely, suppose that $\mathrel{\blacktriangleleft}_{\sqsubset}$ satisfies ($\leq$-left) and ($\mathord{\downarrow}$-right) with respect to $\sqsubseteq$. Let $b\sqsubset a\mathrel{\blacktriangleleft}A$ and $a\mathrel{\blacktriangleleft}B$. Since ${\mathrel{\blacktriangleleft}}\subseteq{\mathrel{\blacktriangleleft}_{\sqsubset}}$, we have $a\mathrel{\mathrel{\blacktriangleleft}_{\sqsubset}}A\downarrow_{\sqsubseteq}B$ by ($\mathord{\downarrow}$-right), so there exists $C\in\mathsf{Fin}(A\downarrow_{\sqsubseteq}B)$ such that $b\ll_{\mathrel{\blacktriangleleft}}C$. Then, there exists $C^{\prime}\in\mathsf{Fin}(A\downarrow_{\sqsubset}B)$ such that $b\mathrel{\blacktriangleleft}C^{\prime}$. ∎

Next, we recall the notions of morphism between basic covers and formal
topologies.

######  Definition .

Let $(S,\mathrel{\lhd})$ and $(S^{\prime},\mathrel{\lhd}^{\prime})$ be basic
covers. A relation $r\subseteq S\times S^{\prime}$ is a _basic cover map_ from
$(S,\mathrel{\lhd})$ to $(S^{\prime},\mathrel{\lhd}^{\prime})$ if

  1. (1)

$a\mathrel{\lhd}r^{-}b\;\rightarrow\>a\mathrel{r}b$,

  2. (2)

$b\mathrel{\lhd}^{\prime}V\;\rightarrow\>r^{-}b\mathrel{\lhd}r^{-}V$.

Basic covers and basic cover maps form a category $\mathsf{BCov}$. The
identity $\mathrm{id}_{(S,\mathrel{\lhd})}$ on a basic cover
$(S,\mathrel{\lhd})$ is defined by

$a\mathrel{\mathrm{id}_{(S,\mathrel{\lhd})}}b\stackrel{{\scriptstyle\textup{def}}}{{\iff}}a\mathrel{\lhd}\left\\{b\right\\},$

and the composition $s*r$ of basic cover maps $r\colon S\to S^{\prime}$ and
$s\colon S^{\prime}\to S^{\prime\prime}$ is defined by

$a\mathrel{(s*r)}c\stackrel{{\scriptstyle\textup{def}}}{{\iff}}a\mathrel{\lhd}r^{-}s^{-}c.$

A _formal topology map_ between formal topologies $(S,\mathrel{\lhd},\leq)$
and $(S^{\prime},\mathrel{\lhd}^{\prime},\leq^{\prime})$ is a basic cover map
$r\colon(S,\mathrel{\lhd})\to(S^{\prime},\mathrel{\lhd}^{\prime})$ such that

  1. (1)

$S\mathrel{\lhd}r^{-}S^{\prime}$,

  2. (2)

$r^{-}a\downarrow_{\leq}r^{-}b\mathrel{\lhd}r^{-}(a\downarrow_{\leq^{\prime}}b)$.

Formal topologies and formal topology maps form a subcategory $\mathsf{FTop}$
of $\mathsf{BCov}$.

In what follows, we extend Proposition 4.5 to morphisms, i.e., we show that
there is a bijective correspondence between join-approximable maps and basic
cover maps, or in the case of localized strong continuous finitary covers,
between proximity maps and formal topology maps (cf. Proposition 4.5). The
correspondence is mediated by an auxiliary notion given in the next lemma.

######  Lemma .

Let $(S,\mathrel{\blacktriangleleft},\sqsubset)$ and
${(S^{\prime}\mathrel{\blacktriangleleft}^{\prime},\sqsubset^{\prime})}$ be
strong continuous finitary covers.

  1. (1)

There exists a bijective correspondence between join-approximable maps from
$S$ to $S^{\prime}$ and relations $r\subseteq S\times S^{\prime}$ satisfying

    1. (a)

$a\mathrel{r}b\leftrightarrow\exists a^{\prime}\in S\left(a\sqsubset
a^{\prime}\mathrel{r}b\right)$,

    2. (b)

$a\mathrel{\blacktriangleleft}A\subseteq r^{-}b\;\rightarrow\>a\mathrel{r}b$,

    3. (c)

$a\mathrel{r}b\mathrel{\blacktriangleleft}^{\prime}B\;\rightarrow\>\exists
A\in\mathsf{Fin}(S)\left(a\mathrel{\blacktriangleleft}A\mathrel{r_{L}}B\right)$,

    4. (d)

$a\mathrel{r}b\sqsubset^{\prime}b^{\prime}\;\rightarrow\>a\mathrel{r}b^{\prime}$,

    5. (e)

$a\mathrel{r}b\;\rightarrow\>\exists A\in\mathsf{Fin}(S)\,\exists
B\in\mathsf{Fin}(S^{\prime})\left(a\mathrel{\blacktriangleleft}A\mathrel{r_{L}}B\sqsubset_{L}^{\prime}\left\\{b\right\\}\right)$.

  2. (2)

If $(S,\mathrel{\blacktriangleleft},\sqsubset)$ and
$(S^{\prime},\mathrel{\blacktriangleleft}^{\prime},\sqsubset^{\prime})$ are
localized, the above bijection restricts to a bijection between proximity maps
and relations between $S$ and $S^{\prime}$ satisfying 1(a)–1(e) above and the
following properties:

    1. (f)

$a\sqsubset a^{\prime}\;\rightarrow\>\exists A\in\mathsf{Fin}(S)\,\exists
B\in\mathsf{Fin}(S^{\prime})(a\mathrel{\blacktriangleleft}A\mathrel{r_{L}}B)$,

    2. (g)

$a\sqsubset
a^{\prime}\mathrel{r}b\mathrel{\,\&\,}a^{\prime}\mathrel{r}c\;\rightarrow\>\exists
A\in\mathsf{Fin}(S)\,\exists
D\in\mathsf{Fin}(b\downarrow_{\sqsubset^{\prime}}c)\left(a\mathrel{\blacktriangleleft}A\mathrel{r}_{L}D\right)$.

###### Proof.

1. If $r\colon(S,\mathrel{\blacktriangleleft},\sqsubset)\to(S^{\prime},\mathrel{\blacktriangleleft}^{\prime},\sqsubset^{\prime})$ is a join-approximable map, then the relation $r^{\dagger}\subseteq S\times S^{\prime}$ defined by

$a\mathrel{r^{\dagger}}b\stackrel{{\scriptstyle\textup{def}}}{{\iff}}a\mathrel{r}\left\\{b\right\\}$
(4.12)

satisfies 1(a)–1(e). Conversely, given a relation $r\subseteq S\times
S^{\prime}$ satisfying 1(a)–1(e), define a relation $r^{*}\subseteq
S\times\mathsf{Fin}(S^{\prime})$ by

$a\mathrel{r^{*}}B\stackrel{{\scriptstyle\textup{def}}}{{\iff}}\exists
A\in\mathsf{Fin}(S)\left(a\mathrel{\blacktriangleleft}A\mathrel{r_{L}}B\right).$
(4.13)

Clearly, $r^{*}$ satisfies (4.8). Moreover, one can easily show
${\mathrel{r^{*}}\mathop{\cdot}{\ll_{\mathrel{\blacktriangleleft}}}}=r^{*}={{\ll_{\mathrel{\blacktriangleleft}^{\prime}}}\mathop{\cdot}\mathrel{r^{*}}}$
using 1(a), 1(c), 1(d), and 1(e). Thus $r^{*}$ is a join-approximable map from
$(S,\mathrel{\blacktriangleleft},\sqsubset)$ to
$(S^{\prime},\mathrel{\blacktriangleleft}^{\prime},\sqsubset^{\prime})$. Then,
it is straightforward to check that above correspondence is bijective (note
that the fact $(r^{*})^{\dagger}=r$ requires 1(b)).

2. Suppose that $(S,\mathrel{\blacktriangleleft},\sqsubset)$ and $(S^{\prime},\mathrel{\blacktriangleleft}^{\prime},\sqsubset^{\prime})$ are localized. First, if $r\colon{(S,\mathrel{\blacktriangleleft},\sqsubset)}\to{(S^{\prime},\mathrel{\blacktriangleleft}^{\prime},\sqsubset^{\prime})}$ is a proximity map, then the relation $r^{\dagger}$ given by (4.12) satisfies 2f and 2g by the fact that $r$ is Lawson and join-approximable (cf. Remark 4.4). Conversely, let $r\subseteq S\times S^{\prime}$ be a relation satisfying 1(a)–2g. Then, the relation $r^{*}$ given by (4.13) satisfies the first property of Lawson approximable map by 2f. For the second property, it suffices to show (4.9). Suppose $a\sqsubset a^{\prime}\mathrel{r^{*}}\left\\{b\right\\}$ and $a^{\prime}\mathrel{r^{*}}\left\\{c\right\\}$. Then, $a^{\prime}\mathrel{r}b$ and $a^{\prime}\mathrel{r}c$ by 1(b). Thus, there exists $D\in{\mathsf{Fin}(b\downarrow_{\sqsubset^{\prime}}c)}$ such that $a\mathrel{r^{*}}D$ by 2g. ∎

######  Proposition .

Let $(S,\mathrel{\blacktriangleleft},\sqsubset)$ and
${(S^{\prime}\mathrel{\blacktriangleleft}^{\prime},\sqsubset^{\prime})}$ be
strong continuous finitary covers.

  1. (1)

There exists a bijective correspondence between join-approximable maps from
$(S,\mathrel{\blacktriangleleft},\sqsubset)$ and
$(S^{\prime},\mathrel{\blacktriangleleft}^{\prime},\sqsubset^{\prime})$ and
basic cover maps from $(S,\mathrel{\blacktriangleleft}_{\sqsubset})$ to
$(S^{\prime},\mathrel{\blacktriangleleft}^{\prime}_{\sqsubset^{\prime}})$.

  2. (2)

If $(S,\mathrel{\blacktriangleleft},\sqsubset)$ and
$(S^{\prime}\mathrel{\blacktriangleleft}^{\prime},\sqsubset^{\prime})$ are
localized, then the above bijection restricts to a bijection between proximity
maps and formal topology maps.

###### Proof.

1. We establish a bijection between basic cover maps from $(S,\mathrel{\blacktriangleleft}_{\sqsubset})$ to $(S^{\prime},\mathrel{\blacktriangleleft}^{\prime}_{\sqsubset^{\prime}})$ and relations between $S$ and $S^{\prime}$ satisfying 1(a)–1(e) in Lemma 4.5. In what follows, we take Proposition 4.5 as given.

First, for a relation $r\subseteq S\times S^{\prime}$ satisfying 1(a)–1(e),
define $\mathchoice{\mathop{\vbox{\halign{#\cr\kern
0.80002pt$\hss\leavevmode\resizebox{3.8315pt}{3.8889pt}{\rotatebox[origin={c}]{90.0}{(}}\hss$\crcr\nointerlineskip\cr$\hss\displaystyle
r\hss$\crcr}}}\limits}{\mathop{\vbox{\halign{#\cr\kern
0.80002pt$\hss\leavevmode\resizebox{3.8315pt}{3.8889pt}{\rotatebox[origin={c}]{90.0}{(}}\hss$\crcr\nointerlineskip\cr$\hss\textstyle
r\hss$\crcr}}}\limits}{\mathop{\vbox{\halign{#\cr\kern
0.80002pt$\hss\leavevmode\resizebox{2.68205pt}{2.72223pt}{\rotatebox[origin={c}]{90.0}{(}}\hss$\crcr\nointerlineskip\cr$\hss\scriptstyle
r\hss$\crcr}}}\limits}{\mathop{\vbox{\halign{#\cr\kern
0.80002pt$\hss\leavevmode\resizebox{1.91574pt}{1.94444pt}{\rotatebox[origin={c}]{90.0}{(}}\hss$\crcr\nointerlineskip\cr$\hss\scriptscriptstyle
r\hss$\crcr}}}\limits}\subseteq S\times S^{\prime}$ by

$a\mathrel{\mathchoice{\mathop{\vbox{\halign{#\cr\kern
0.80002pt$\hss\leavevmode\resizebox{3.8315pt}{3.8889pt}{\rotatebox[origin={c}]{90.0}{(}}\hss$\crcr\nointerlineskip\cr$\hss\displaystyle
r\hss$\crcr}}}\limits}{\mathop{\vbox{\halign{#\cr\kern
0.80002pt$\hss\leavevmode\resizebox{3.8315pt}{3.8889pt}{\rotatebox[origin={c}]{90.0}{(}}\hss$\crcr\nointerlineskip\cr$\hss\textstyle
r\hss$\crcr}}}\limits}{\mathop{\vbox{\halign{#\cr\kern
0.80002pt$\hss\leavevmode\resizebox{2.68205pt}{2.72223pt}{\rotatebox[origin={c}]{90.0}{(}}\hss$\crcr\nointerlineskip\cr$\hss\scriptstyle
r\hss$\crcr}}}\limits}{\mathop{\vbox{\halign{#\cr\kern
0.80002pt$\hss\leavevmode\resizebox{1.91574pt}{1.94444pt}{\rotatebox[origin={c}]{90.0}{(}}\hss$\crcr\nointerlineskip\cr$\hss\scriptscriptstyle
r\hss$\crcr}}}\limits}}b\stackrel{{\scriptstyle\textup{def}}}{{\iff}}a\mathrel{\mathrel{\blacktriangleleft}_{\sqsubset}}r^{-}b.$
(4.14)

We show that $\mathchoice{\mathop{\vbox{\halign{#\cr\kern
0.80002pt$\hss\leavevmode\resizebox{3.8315pt}{3.8889pt}{\rotatebox[origin={c}]{90.0}{(}}\hss$\crcr\nointerlineskip\cr$\hss\displaystyle
r\hss$\crcr}}}\limits}{\mathop{\vbox{\halign{#\cr\kern
0.80002pt$\hss\leavevmode\resizebox{3.8315pt}{3.8889pt}{\rotatebox[origin={c}]{90.0}{(}}\hss$\crcr\nointerlineskip\cr$\hss\textstyle
r\hss$\crcr}}}\limits}{\mathop{\vbox{\halign{#\cr\kern
0.80002pt$\hss\leavevmode\resizebox{2.68205pt}{2.72223pt}{\rotatebox[origin={c}]{90.0}{(}}\hss$\crcr\nointerlineskip\cr$\hss\scriptstyle
r\hss$\crcr}}}\limits}{\mathop{\vbox{\halign{#\cr\kern
0.80002pt$\hss\leavevmode\resizebox{1.91574pt}{1.94444pt}{\rotatebox[origin={c}]{90.0}{(}}\hss$\crcr\nointerlineskip\cr$\hss\scriptscriptstyle
r\hss$\crcr}}}\limits}$ satisfies 1 and 2.

1 This follows from (transitivity) of
$\mathrel{\blacktriangleleft}_{\sqsubset}$.

2 Suppose
$b\mathrel{\mathrel{\blacktriangleleft}^{\prime}_{\sqsubset^{\prime}}}V$ and
$a\mathrel{\mathchoice{\mathop{\vbox{\halign{#\cr\kern
0.80002pt$\hss\leavevmode\resizebox{3.8315pt}{3.8889pt}{\rotatebox[origin={c}]{90.0}{(}}\hss$\crcr\nointerlineskip\cr$\hss\displaystyle
r\hss$\crcr}}}\limits}{\mathop{\vbox{\halign{#\cr\kern
0.80002pt$\hss\leavevmode\resizebox{3.8315pt}{3.8889pt}{\rotatebox[origin={c}]{90.0}{(}}\hss$\crcr\nointerlineskip\cr$\hss\textstyle
r\hss$\crcr}}}\limits}{\mathop{\vbox{\halign{#\cr\kern
0.80002pt$\hss\leavevmode\resizebox{2.68205pt}{2.72223pt}{\rotatebox[origin={c}]{90.0}{(}}\hss$\crcr\nointerlineskip\cr$\hss\scriptstyle
r\hss$\crcr}}}\limits}{\mathop{\vbox{\halign{#\cr\kern
0.80002pt$\hss\leavevmode\resizebox{1.91574pt}{1.94444pt}{\rotatebox[origin={c}]{90.0}{(}}\hss$\crcr\nointerlineskip\cr$\hss\scriptscriptstyle
r\hss$\crcr}}}\limits}}b$. Since
$a\mathrel{\mathrel{\blacktriangleleft}_{\sqsubset}}r^{-}b$, we may assume
$a\mathrel{r}b$ by (transitivity). By 1(e), there exists $A\in\mathsf{Fin}(S)$
and $B\in\mathsf{Fin}(S^{\prime})$ such that
$a\mathrel{\blacktriangleleft}A\mathrel{r_{L}}B\sqsubset_{L}^{\prime}\left\\{b\right\\}$.
Since $b\mathrel{\blacktriangleleft}^{\prime}_{\sqsubset^{\prime}}V$, there
exist $B^{\prime},B^{\prime\prime}\in\mathsf{Fin}(S^{\prime})$ such that
$B\mathrel{\widetilde{\mathrel{\blacktriangleleft}^{\prime}}}B^{\prime}\sqsubset_{L}^{\prime}B^{\prime\prime}\subseteq
V$. By 1(c), there exists $A^{\prime}\in\mathsf{Fin}(S)$ such that
$A\mathrel{\widetilde{\mathrel{\blacktriangleleft}}}A^{\prime}\mathrel{r_{L}}B^{\prime}$,
and so $A^{\prime}\mathrel{r_{L}}B^{\prime\prime}$ by 1(d). Then,
$a\mathrel{\blacktriangleleft}A^{\prime}\in\mathsf{Fin}(\mathchoice{\mathop{\vbox{\halign{#\cr\kern
0.80002pt$\hss\leavevmode\resizebox{3.8315pt}{3.8889pt}{\rotatebox[origin={c}]{90.0}{(}}\hss$\crcr\nointerlineskip\cr$\hss\displaystyle
r\hss$\crcr}}}\limits}{\mathop{\vbox{\halign{#\cr\kern
0.80002pt$\hss\leavevmode\resizebox{3.8315pt}{3.8889pt}{\rotatebox[origin={c}]{90.0}{(}}\hss$\crcr\nointerlineskip\cr$\hss\textstyle
r\hss$\crcr}}}\limits}{\mathop{\vbox{\halign{#\cr\kern
0.80002pt$\hss\leavevmode\resizebox{2.68205pt}{2.72223pt}{\rotatebox[origin={c}]{90.0}{(}}\hss$\crcr\nointerlineskip\cr$\hss\scriptstyle
r\hss$\crcr}}}\limits}{\mathop{\vbox{\halign{#\cr\kern
0.80002pt$\hss\leavevmode\resizebox{1.91574pt}{1.94444pt}{\rotatebox[origin={c}]{90.0}{(}}\hss$\crcr\nointerlineskip\cr$\hss\scriptscriptstyle
r\hss$\crcr}}}\limits}^{-}V)$ so that
$a\mathrel{\blacktriangleleft}_{\sqsubset}\mathchoice{\mathop{\vbox{\halign{#\cr\kern
0.80002pt$\hss\leavevmode\resizebox{3.8315pt}{3.8889pt}{\rotatebox[origin={c}]{90.0}{(}}\hss$\crcr\nointerlineskip\cr$\hss\displaystyle
r\hss$\crcr}}}\limits}{\mathop{\vbox{\halign{#\cr\kern
0.80002pt$\hss\leavevmode\resizebox{3.8315pt}{3.8889pt}{\rotatebox[origin={c}]{90.0}{(}}\hss$\crcr\nointerlineskip\cr$\hss\textstyle
r\hss$\crcr}}}\limits}{\mathop{\vbox{\halign{#\cr\kern
0.80002pt$\hss\leavevmode\resizebox{2.68205pt}{2.72223pt}{\rotatebox[origin={c}]{90.0}{(}}\hss$\crcr\nointerlineskip\cr$\hss\scriptstyle
r\hss$\crcr}}}\limits}{\mathop{\vbox{\halign{#\cr\kern
0.80002pt$\hss\leavevmode\resizebox{1.91574pt}{1.94444pt}{\rotatebox[origin={c}]{90.0}{(}}\hss$\crcr\nointerlineskip\cr$\hss\scriptscriptstyle
r\hss$\crcr}}}\limits}^{-}V$. Hence,
$\mathchoice{\mathop{\vbox{\halign{#\cr\kern
0.80002pt$\hss\leavevmode\resizebox{3.8315pt}{3.8889pt}{\rotatebox[origin={c}]{90.0}{(}}\hss$\crcr\nointerlineskip\cr$\hss\displaystyle
r\hss$\crcr}}}\limits}{\mathop{\vbox{\halign{#\cr\kern
0.80002pt$\hss\leavevmode\resizebox{3.8315pt}{3.8889pt}{\rotatebox[origin={c}]{90.0}{(}}\hss$\crcr\nointerlineskip\cr$\hss\textstyle
r\hss$\crcr}}}\limits}{\mathop{\vbox{\halign{#\cr\kern
0.80002pt$\hss\leavevmode\resizebox{2.68205pt}{2.72223pt}{\rotatebox[origin={c}]{90.0}{(}}\hss$\crcr\nointerlineskip\cr$\hss\scriptstyle
r\hss$\crcr}}}\limits}{\mathop{\vbox{\halign{#\cr\kern
0.80002pt$\hss\leavevmode\resizebox{1.91574pt}{1.94444pt}{\rotatebox[origin={c}]{90.0}{(}}\hss$\crcr\nointerlineskip\cr$\hss\scriptscriptstyle
r\hss$\crcr}}}\limits}^{-}b\mathrel{\blacktriangleleft}_{\sqsubset}\mathchoice{\mathop{\vbox{\halign{#\cr\kern
0.80002pt$\hss\leavevmode\resizebox{3.8315pt}{3.8889pt}{\rotatebox[origin={c}]{90.0}{(}}\hss$\crcr\nointerlineskip\cr$\hss\displaystyle
r\hss$\crcr}}}\limits}{\mathop{\vbox{\halign{#\cr\kern
0.80002pt$\hss\leavevmode\resizebox{3.8315pt}{3.8889pt}{\rotatebox[origin={c}]{90.0}{(}}\hss$\crcr\nointerlineskip\cr$\hss\textstyle
r\hss$\crcr}}}\limits}{\mathop{\vbox{\halign{#\cr\kern
0.80002pt$\hss\leavevmode\resizebox{2.68205pt}{2.72223pt}{\rotatebox[origin={c}]{90.0}{(}}\hss$\crcr\nointerlineskip\cr$\hss\scriptstyle
r\hss$\crcr}}}\limits}{\mathop{\vbox{\halign{#\cr\kern
0.80002pt$\hss\leavevmode\resizebox{1.91574pt}{1.94444pt}{\rotatebox[origin={c}]{90.0}{(}}\hss$\crcr\nointerlineskip\cr$\hss\scriptscriptstyle
r\hss$\crcr}}}\limits}^{-}V$.

Conversely, for a basic cover map
$r\colon(S,\mathrel{\blacktriangleleft}_{\sqsubset})\to(S^{\prime},\mathrel{\blacktriangleleft}^{\prime}_{\sqsubset^{\prime}})$,
define a relation $r^{\ddagger}\subseteq S\times S^{\prime}$ by

$a\mathrel{r^{\ddagger}}b\stackrel{{\scriptstyle\textup{def}}}{{\iff}}a\in\mathord{\downarrow}_{\sqsubset}r^{-}b.$
(4.15)

We show that $r^{\ddagger}$ satisfies 1(a)–1(e) in Lemma 4.5.

1(a) This follows from the idempotency of $\sqsubset$.

1(b) Let $a\mathrel{\blacktriangleleft}A\subseteq(r^{\ddagger})^{-}b$. Then,
there exists $A^{\prime}\in\mathsf{Fin}(r^{-}b)$ such that
$A\sqsubset_{L}A^{\prime}$. Since $S$ is strong, there exists $a^{\prime}$
such that $a\sqsubset a^{\prime}\mathrel{\blacktriangleleft}A^{\prime}$. Then,
$a^{\prime}\mathrel{\blacktriangleleft}_{\sqsubset}A^{\prime}$ and so
$a^{\prime}\mathrel{r}b$ by 1. Hence $a\mathrel{r^{\ddagger}}b$.

1(c) Let $a\mathrel{r^{\ddagger}}b\mathrel{\blacktriangleleft}^{\prime}B$.
Then, there exists $a^{\prime}$ such that $a\sqsubset a^{\prime}\mathrel{r}b$.
Since $b\mathrel{\blacktriangleleft}^{\prime}_{\sqsubset^{\prime}}B$, we have
$r^{-}b\mathrel{\blacktriangleleft}_{\sqsubset}r^{-}B$ by 2, so there exists
$A\in\mathsf{Fin}(r^{-}B)$ such that $a\ll_{\mathrel{\blacktriangleleft}}A$.
Thus, there exists $A^{\prime}\sqsubset_{L}A$ such that
$a\mathrel{\blacktriangleleft}A^{\prime}$ and
$A^{\prime}\mathrel{(r^{\ddagger})_{L}}B$.

1(d) Let $a\mathrel{r^{\ddagger}}b\sqsubset^{\prime}b^{\prime}$. Then, there
exists $a^{\prime}$ such that $a\sqsubset a^{\prime}\mathrel{r}b$. Since
$b\sqsubset^{\prime}b^{\prime}$ implies
$b\mathrel{\blacktriangleleft}^{\prime}_{\sqsubset^{\prime}}\left\\{b^{\prime}\right\\}$,
we have $r^{-}b\mathrel{\blacktriangleleft}_{\sqsubset}r^{-}b^{\prime}$ by 2.
Then $a^{\prime}\mathrel{r}b^{\prime}$ by 1 so that
$a\mathrel{r^{\ddagger}}b^{\prime}$.

1(e) Let $a\mathrel{r^{\ddagger}}b$. Then, there exists $a^{\prime}$ such that
$a\sqsubset a^{\prime}\mathrel{r}b$. Since
$b\mathrel{\blacktriangleleft}^{\prime}_{\sqsubset^{\prime}}\mathord{\downarrow}_{\sqsubset^{\prime}}b$,
we have
$a^{\prime}\mathrel{\blacktriangleleft}_{\sqsubset}r^{-}\mathord{\downarrow}_{\sqsubset^{\prime}}b$
by 2. Thus, there exists
$A\in\mathsf{Fin}(r^{-}\mathord{\downarrow}_{\sqsubset^{\prime}}b)$ such that
$a\ll_{\mathrel{\blacktriangleleft}}A$, and so there exist
$A^{\prime}\in\mathsf{Fin}(S)$ and $B\sqsubset_{L}^{\prime}\left\\{b\right\\}$
such that $a\mathrel{\blacktriangleleft}A^{\prime}\sqsubset_{L}A$ and
$A\mathrel{r_{L}}B$. Then, $A^{\prime}\mathrel{(r^{\ddagger})_{L}}B$.

Next, we show that the above correspondence is bijective. First, note that

$a\mathrel{\blacktriangleleft}_{\sqsubset}U\iff
a\mathrel{\blacktriangleleft}_{\sqsubset}\mathord{\downarrow}_{\sqsubset}U$
(4.16)

for each $a\in S$ and $U\subseteq S$. Thus, for any basic cover map
$r\colon{(S,\mathrel{\blacktriangleleft}_{\sqsubset})}\to{(S^{\prime},\mathrel{\blacktriangleleft}^{\prime}_{\sqsubset^{\prime}})}$,
we have

$\displaystyle a\mathrel{\mathchoice{\mathop{\vbox{\halign{#\cr\kern
0.80002pt$\hss\leavevmode\resizebox{5.82262pt}{3.8889pt}{\rotatebox[origin={c}]{90.0}{(}}\hss$\crcr\nointerlineskip\cr$\hss\displaystyle
r^{\ddagger}\hss$\crcr}}}\limits}{\mathop{\vbox{\halign{#\cr\kern
0.80002pt$\hss\leavevmode\resizebox{5.82262pt}{3.8889pt}{\rotatebox[origin={c}]{90.0}{(}}\hss$\crcr\nointerlineskip\cr$\hss\textstyle
r^{\ddagger}\hss$\crcr}}}\limits}{\mathop{\vbox{\halign{#\cr\kern
0.80002pt$\hss\leavevmode\resizebox{4.10426pt}{2.72223pt}{\rotatebox[origin={c}]{90.0}{(}}\hss$\crcr\nointerlineskip\cr$\hss\scriptstyle
r^{\ddagger}\hss$\crcr}}}\limits}{\mathop{\vbox{\halign{#\cr\kern
0.80002pt$\hss\leavevmode\resizebox{3.33795pt}{1.94444pt}{\rotatebox[origin={c}]{90.0}{(}}\hss$\crcr\nointerlineskip\cr$\hss\scriptscriptstyle
r^{\ddagger}\hss$\crcr}}}\limits}}b$ $\displaystyle\iff
a\mathrel{\blacktriangleleft}_{\sqsubset}(r^{\ddagger})^{-}b$
$\displaystyle\iff a\mathrel{\blacktriangleleft}_{\sqsubset}r^{-}b$ (by
(4.16)) $\displaystyle\iff a\mathrel{r}b$ $\displaystyle\text{(by
\ref{BCM1})}.$

Conversely, for any relation $r\subseteq S\times S^{\prime}$ satisfying
1(a)–1(e), we have

$\displaystyle a\mathrel{(\mathchoice{\mathop{\vbox{\halign{#\cr\kern
0.80002pt$\hss\leavevmode\resizebox{3.8315pt}{3.8889pt}{\rotatebox[origin={c}]{90.0}{(}}\hss$\crcr\nointerlineskip\cr$\hss\displaystyle
r\hss$\crcr}}}\limits}{\mathop{\vbox{\halign{#\cr\kern
0.80002pt$\hss\leavevmode\resizebox{3.8315pt}{3.8889pt}{\rotatebox[origin={c}]{90.0}{(}}\hss$\crcr\nointerlineskip\cr$\hss\textstyle
r\hss$\crcr}}}\limits}{\mathop{\vbox{\halign{#\cr\kern
0.80002pt$\hss\leavevmode\resizebox{2.68205pt}{2.72223pt}{\rotatebox[origin={c}]{90.0}{(}}\hss$\crcr\nointerlineskip\cr$\hss\scriptstyle
r\hss$\crcr}}}\limits}{\mathop{\vbox{\halign{#\cr\kern
0.80002pt$\hss\leavevmode\resizebox{1.91574pt}{1.94444pt}{\rotatebox[origin={c}]{90.0}{(}}\hss$\crcr\nointerlineskip\cr$\hss\scriptscriptstyle
r\hss$\crcr}}}\limits})^{\ddagger}}b$ $\displaystyle\iff\exists a^{\prime}\in
S\left(a\sqsubset
a^{\prime}\mathrel{\blacktriangleleft}_{\sqsubset}r^{-}b\right)$
$\displaystyle\iff\exists
A\in\mathsf{Fin}(r^{-}b)\,a\ll_{\mathrel{\blacktriangleleft}}A$ (by
${\mathrel{\blacktriangleleft}}\subseteq{\mathrel{\blacktriangleleft}_{\sqsubset}}$)
$\displaystyle\iff\exists
A\in\mathsf{Fin}(r^{-}b)\,a\mathrel{\blacktriangleleft}A$ (by 1(a))
$\displaystyle\iff a\mathrel{r}b$ $\displaystyle\text{(by
\ref{lem:SingleVersionJoinPresAppMap2})}.$

2. Suppose that $(S,\mathrel{\blacktriangleleft},\sqsubset)$ and $(S^{\prime},\mathrel{\blacktriangleleft}^{\prime},\sqsubset^{\prime})$ are localized. First, let $r\subseteq S\times S^{\prime}$ be a relation satisfying 1(a)–2g in Lemma 4.5. We must show that $\mathchoice{\mathop{\vbox{\halign{#\cr\kern 0.80002pt$\hss\leavevmode\resizebox{3.8315pt}{3.8889pt}{\rotatebox[origin={c}]{90.0}{(}}\hss$\crcr\nointerlineskip\cr$\hss\displaystyle r\hss$\crcr}}}\limits}{\mathop{\vbox{\halign{#\cr\kern 0.80002pt$\hss\leavevmode\resizebox{3.8315pt}{3.8889pt}{\rotatebox[origin={c}]{90.0}{(}}\hss$\crcr\nointerlineskip\cr$\hss\textstyle r\hss$\crcr}}}\limits}{\mathop{\vbox{\halign{#\cr\kern 0.80002pt$\hss\leavevmode\resizebox{2.68205pt}{2.72223pt}{\rotatebox[origin={c}]{90.0}{(}}\hss$\crcr\nointerlineskip\cr$\hss\scriptstyle r\hss$\crcr}}}\limits}{\mathop{\vbox{\halign{#\cr\kern 0.80002pt$\hss\leavevmode\resizebox{1.91574pt}{1.94444pt}{\rotatebox[origin={c}]{90.0}{(}}\hss$\crcr\nointerlineskip\cr$\hss\scriptscriptstyle r\hss$\crcr}}}\limits}$ given by (4.14) satisfies 1 and 2.

1 Let $a\in S$ and $a^{\prime}\sqsubset a$. Choose $a^{\prime\prime}\in S$
such that $a^{\prime}\sqsubset a^{\prime\prime}\sqsubset a$. By 2f, there
exist $A\in\mathsf{Fin}(S)$ and $B\in\mathsf{Fin}(S^{\prime})$ such that
$a^{\prime\prime}\mathrel{\blacktriangleleft}A\mathrel{r_{L}}B$. Then,
$a^{\prime}\ll_{\mathrel{\blacktriangleleft}}A$ and
$A\subseteq(\mathchoice{\mathop{\vbox{\halign{#\cr\kern
0.80002pt$\hss\leavevmode\resizebox{3.8315pt}{3.8889pt}{\rotatebox[origin={c}]{90.0}{(}}\hss$\crcr\nointerlineskip\cr$\hss\displaystyle
r\hss$\crcr}}}\limits}{\mathop{\vbox{\halign{#\cr\kern
0.80002pt$\hss\leavevmode\resizebox{3.8315pt}{3.8889pt}{\rotatebox[origin={c}]{90.0}{(}}\hss$\crcr\nointerlineskip\cr$\hss\textstyle
r\hss$\crcr}}}\limits}{\mathop{\vbox{\halign{#\cr\kern
0.80002pt$\hss\leavevmode\resizebox{2.68205pt}{2.72223pt}{\rotatebox[origin={c}]{90.0}{(}}\hss$\crcr\nointerlineskip\cr$\hss\scriptstyle
r\hss$\crcr}}}\limits}{\mathop{\vbox{\halign{#\cr\kern
0.80002pt$\hss\leavevmode\resizebox{1.91574pt}{1.94444pt}{\rotatebox[origin={c}]{90.0}{(}}\hss$\crcr\nointerlineskip\cr$\hss\scriptscriptstyle
r\hss$\crcr}}}\limits})^{-}B$. Thus
$a\mathrel{\blacktriangleleft}_{\sqsubset}(\mathchoice{\mathop{\vbox{\halign{#\cr\kern
0.80002pt$\hss\leavevmode\resizebox{3.8315pt}{3.8889pt}{\rotatebox[origin={c}]{90.0}{(}}\hss$\crcr\nointerlineskip\cr$\hss\displaystyle
r\hss$\crcr}}}\limits}{\mathop{\vbox{\halign{#\cr\kern
0.80002pt$\hss\leavevmode\resizebox{3.8315pt}{3.8889pt}{\rotatebox[origin={c}]{90.0}{(}}\hss$\crcr\nointerlineskip\cr$\hss\textstyle
r\hss$\crcr}}}\limits}{\mathop{\vbox{\halign{#\cr\kern
0.80002pt$\hss\leavevmode\resizebox{2.68205pt}{2.72223pt}{\rotatebox[origin={c}]{90.0}{(}}\hss$\crcr\nointerlineskip\cr$\hss\scriptstyle
r\hss$\crcr}}}\limits}{\mathop{\vbox{\halign{#\cr\kern
0.80002pt$\hss\leavevmode\resizebox{1.91574pt}{1.94444pt}{\rotatebox[origin={c}]{90.0}{(}}\hss$\crcr\nointerlineskip\cr$\hss\scriptscriptstyle
r\hss$\crcr}}}\limits})^{-}B\subseteq(\mathchoice{\mathop{\vbox{\halign{#\cr\kern
0.80002pt$\hss\leavevmode\resizebox{3.8315pt}{3.8889pt}{\rotatebox[origin={c}]{90.0}{(}}\hss$\crcr\nointerlineskip\cr$\hss\displaystyle
r\hss$\crcr}}}\limits}{\mathop{\vbox{\halign{#\cr\kern
0.80002pt$\hss\leavevmode\resizebox{3.8315pt}{3.8889pt}{\rotatebox[origin={c}]{90.0}{(}}\hss$\crcr\nointerlineskip\cr$\hss\textstyle
r\hss$\crcr}}}\limits}{\mathop{\vbox{\halign{#\cr\kern
0.80002pt$\hss\leavevmode\resizebox{2.68205pt}{2.72223pt}{\rotatebox[origin={c}]{90.0}{(}}\hss$\crcr\nointerlineskip\cr$\hss\scriptstyle
r\hss$\crcr}}}\limits}{\mathop{\vbox{\halign{#\cr\kern
0.80002pt$\hss\leavevmode\resizebox{1.91574pt}{1.94444pt}{\rotatebox[origin={c}]{90.0}{(}}\hss$\crcr\nointerlineskip\cr$\hss\scriptscriptstyle
r\hss$\crcr}}}\limits})^{-}S^{\prime}$, and hence
$S\mathrel{\blacktriangleleft}_{\sqsubset}(\mathchoice{\mathop{\vbox{\halign{#\cr\kern
0.80002pt$\hss\leavevmode\resizebox{3.8315pt}{3.8889pt}{\rotatebox[origin={c}]{90.0}{(}}\hss$\crcr\nointerlineskip\cr$\hss\displaystyle
r\hss$\crcr}}}\limits}{\mathop{\vbox{\halign{#\cr\kern
0.80002pt$\hss\leavevmode\resizebox{3.8315pt}{3.8889pt}{\rotatebox[origin={c}]{90.0}{(}}\hss$\crcr\nointerlineskip\cr$\hss\textstyle
r\hss$\crcr}}}\limits}{\mathop{\vbox{\halign{#\cr\kern
0.80002pt$\hss\leavevmode\resizebox{2.68205pt}{2.72223pt}{\rotatebox[origin={c}]{90.0}{(}}\hss$\crcr\nointerlineskip\cr$\hss\scriptstyle
r\hss$\crcr}}}\limits}{\mathop{\vbox{\halign{#\cr\kern
0.80002pt$\hss\leavevmode\resizebox{1.91574pt}{1.94444pt}{\rotatebox[origin={c}]{90.0}{(}}\hss$\crcr\nointerlineskip\cr$\hss\scriptscriptstyle
r\hss$\crcr}}}\limits})^{-}S^{\prime}$.

2 Let $a\in\mathchoice{\mathop{\vbox{\halign{#\cr\kern
0.80002pt$\hss\leavevmode\resizebox{3.8315pt}{3.8889pt}{\rotatebox[origin={c}]{90.0}{(}}\hss$\crcr\nointerlineskip\cr$\hss\displaystyle
r\hss$\crcr}}}\limits}{\mathop{\vbox{\halign{#\cr\kern
0.80002pt$\hss\leavevmode\resizebox{3.8315pt}{3.8889pt}{\rotatebox[origin={c}]{90.0}{(}}\hss$\crcr\nointerlineskip\cr$\hss\textstyle
r\hss$\crcr}}}\limits}{\mathop{\vbox{\halign{#\cr\kern
0.80002pt$\hss\leavevmode\resizebox{2.68205pt}{2.72223pt}{\rotatebox[origin={c}]{90.0}{(}}\hss$\crcr\nointerlineskip\cr$\hss\scriptstyle
r\hss$\crcr}}}\limits}{\mathop{\vbox{\halign{#\cr\kern
0.80002pt$\hss\leavevmode\resizebox{1.91574pt}{1.94444pt}{\rotatebox[origin={c}]{90.0}{(}}\hss$\crcr\nointerlineskip\cr$\hss\scriptscriptstyle
r\hss$\crcr}}}\limits}^{-}b\downarrow_{\sqsubseteq}\mathchoice{\mathop{\vbox{\halign{#\cr\kern
0.80002pt$\hss\leavevmode\resizebox{3.8315pt}{3.8889pt}{\rotatebox[origin={c}]{90.0}{(}}\hss$\crcr\nointerlineskip\cr$\hss\displaystyle
r\hss$\crcr}}}\limits}{\mathop{\vbox{\halign{#\cr\kern
0.80002pt$\hss\leavevmode\resizebox{3.8315pt}{3.8889pt}{\rotatebox[origin={c}]{90.0}{(}}\hss$\crcr\nointerlineskip\cr$\hss\textstyle
r\hss$\crcr}}}\limits}{\mathop{\vbox{\halign{#\cr\kern
0.80002pt$\hss\leavevmode\resizebox{2.68205pt}{2.72223pt}{\rotatebox[origin={c}]{90.0}{(}}\hss$\crcr\nointerlineskip\cr$\hss\scriptstyle
r\hss$\crcr}}}\limits}{\mathop{\vbox{\halign{#\cr\kern
0.80002pt$\hss\leavevmode\resizebox{1.91574pt}{1.94444pt}{\rotatebox[origin={c}]{90.0}{(}}\hss$\crcr\nointerlineskip\cr$\hss\scriptscriptstyle
r\hss$\crcr}}}\limits}^{-}c$. By ($\leq$-left), we have
$a\mathrel{\blacktriangleleft}_{\sqsubset}r^{-}b$ and
$a\mathrel{\blacktriangleleft}_{\sqsubset}r^{-}c$, and so
$a\mathrel{\blacktriangleleft}_{\sqsubset}r^{-}b\downarrow_{\sqsubseteq}r^{-}c$
by ($\mathord{\downarrow}$-right). By (transitivity), it suffices to show
$r^{-}b\downarrow_{\sqsubseteq}r^{-}c\mathrel{\blacktriangleleft}_{\sqsubset}(\mathchoice{\mathop{\vbox{\halign{#\cr\kern
0.80002pt$\hss\leavevmode\resizebox{3.8315pt}{3.8889pt}{\rotatebox[origin={c}]{90.0}{(}}\hss$\crcr\nointerlineskip\cr$\hss\displaystyle
r\hss$\crcr}}}\limits}{\mathop{\vbox{\halign{#\cr\kern
0.80002pt$\hss\leavevmode\resizebox{3.8315pt}{3.8889pt}{\rotatebox[origin={c}]{90.0}{(}}\hss$\crcr\nointerlineskip\cr$\hss\textstyle
r\hss$\crcr}}}\limits}{\mathop{\vbox{\halign{#\cr\kern
0.80002pt$\hss\leavevmode\resizebox{2.68205pt}{2.72223pt}{\rotatebox[origin={c}]{90.0}{(}}\hss$\crcr\nointerlineskip\cr$\hss\scriptstyle
r\hss$\crcr}}}\limits}{\mathop{\vbox{\halign{#\cr\kern
0.80002pt$\hss\leavevmode\resizebox{1.91574pt}{1.94444pt}{\rotatebox[origin={c}]{90.0}{(}}\hss$\crcr\nointerlineskip\cr$\hss\scriptscriptstyle
r\hss$\crcr}}}\limits})^{-}\left(b\downarrow_{\sqsubseteq^{\prime}}c\right)$.
Let $a^{\prime}\in r^{-}b\downarrow_{\sqsubseteq}r^{-}c$, and
$a^{\prime\prime}\sqsubset a^{\prime}$. Choose $a^{\prime\prime\prime}\in S$
such that $a^{\prime\prime}\sqsubset a^{\prime\prime\prime}\sqsubset
a^{\prime}$. We have $r^{-}b\downarrow_{\sqsubseteq}r^{-}c=r^{-}b\cap r^{-}c$
by 1(a), so by applying 2g, we find $A\in\mathsf{Fin}(S)$ and
$D\in\mathsf{Fin}(b\downarrow_{\sqsubset^{\prime}}c)$ such that
$a^{\prime\prime\prime}\mathrel{\blacktriangleleft}A\mathrel{r_{L}}D$. Then,
$a^{\prime\prime}\ll_{\mathrel{\blacktriangleleft}}A$ and
$A\subseteq(\mathchoice{\mathop{\vbox{\halign{#\cr\kern
0.80002pt$\hss\leavevmode\resizebox{3.8315pt}{3.8889pt}{\rotatebox[origin={c}]{90.0}{(}}\hss$\crcr\nointerlineskip\cr$\hss\displaystyle
r\hss$\crcr}}}\limits}{\mathop{\vbox{\halign{#\cr\kern
0.80002pt$\hss\leavevmode\resizebox{3.8315pt}{3.8889pt}{\rotatebox[origin={c}]{90.0}{(}}\hss$\crcr\nointerlineskip\cr$\hss\textstyle
r\hss$\crcr}}}\limits}{\mathop{\vbox{\halign{#\cr\kern
0.80002pt$\hss\leavevmode\resizebox{2.68205pt}{2.72223pt}{\rotatebox[origin={c}]{90.0}{(}}\hss$\crcr\nointerlineskip\cr$\hss\scriptstyle
r\hss$\crcr}}}\limits}{\mathop{\vbox{\halign{#\cr\kern
0.80002pt$\hss\leavevmode\resizebox{1.91574pt}{1.94444pt}{\rotatebox[origin={c}]{90.0}{(}}\hss$\crcr\nointerlineskip\cr$\hss\scriptscriptstyle
r\hss$\crcr}}}\limits})^{-}D\subseteq(\mathchoice{\mathop{\vbox{\halign{#\cr\kern
0.80002pt$\hss\leavevmode\resizebox{3.8315pt}{3.8889pt}{\rotatebox[origin={c}]{90.0}{(}}\hss$\crcr\nointerlineskip\cr$\hss\displaystyle
r\hss$\crcr}}}\limits}{\mathop{\vbox{\halign{#\cr\kern
0.80002pt$\hss\leavevmode\resizebox{3.8315pt}{3.8889pt}{\rotatebox[origin={c}]{90.0}{(}}\hss$\crcr\nointerlineskip\cr$\hss\textstyle
r\hss$\crcr}}}\limits}{\mathop{\vbox{\halign{#\cr\kern
0.80002pt$\hss\leavevmode\resizebox{2.68205pt}{2.72223pt}{\rotatebox[origin={c}]{90.0}{(}}\hss$\crcr\nointerlineskip\cr$\hss\scriptstyle
r\hss$\crcr}}}\limits}{\mathop{\vbox{\halign{#\cr\kern
0.80002pt$\hss\leavevmode\resizebox{1.91574pt}{1.94444pt}{\rotatebox[origin={c}]{90.0}{(}}\hss$\crcr\nointerlineskip\cr$\hss\scriptscriptstyle
r\hss$\crcr}}}\limits})^{-}(b\downarrow_{\sqsubseteq^{\prime}}c)$, and so
$a^{\prime}\mathrel{\blacktriangleleft}_{\sqsubset}(\mathchoice{\mathop{\vbox{\halign{#\cr\kern
0.80002pt$\hss\leavevmode\resizebox{3.8315pt}{3.8889pt}{\rotatebox[origin={c}]{90.0}{(}}\hss$\crcr\nointerlineskip\cr$\hss\displaystyle
r\hss$\crcr}}}\limits}{\mathop{\vbox{\halign{#\cr\kern
0.80002pt$\hss\leavevmode\resizebox{3.8315pt}{3.8889pt}{\rotatebox[origin={c}]{90.0}{(}}\hss$\crcr\nointerlineskip\cr$\hss\textstyle
r\hss$\crcr}}}\limits}{\mathop{\vbox{\halign{#\cr\kern
0.80002pt$\hss\leavevmode\resizebox{2.68205pt}{2.72223pt}{\rotatebox[origin={c}]{90.0}{(}}\hss$\crcr\nointerlineskip\cr$\hss\scriptstyle
r\hss$\crcr}}}\limits}{\mathop{\vbox{\halign{#\cr\kern
0.80002pt$\hss\leavevmode\resizebox{1.91574pt}{1.94444pt}{\rotatebox[origin={c}]{90.0}{(}}\hss$\crcr\nointerlineskip\cr$\hss\scriptscriptstyle
r\hss$\crcr}}}\limits})^{-}\left(b\downarrow_{\sqsubseteq^{\prime}}c\right)$.
Hence,
$r^{-}b\downarrow_{\sqsubseteq}r^{-}c\mathrel{\blacktriangleleft}_{\sqsubset}(\mathchoice{\mathop{\vbox{\halign{#\cr\kern
0.80002pt$\hss\leavevmode\resizebox{3.8315pt}{3.8889pt}{\rotatebox[origin={c}]{90.0}{(}}\hss$\crcr\nointerlineskip\cr$\hss\displaystyle
r\hss$\crcr}}}\limits}{\mathop{\vbox{\halign{#\cr\kern
0.80002pt$\hss\leavevmode\resizebox{3.8315pt}{3.8889pt}{\rotatebox[origin={c}]{90.0}{(}}\hss$\crcr\nointerlineskip\cr$\hss\textstyle
r\hss$\crcr}}}\limits}{\mathop{\vbox{\halign{#\cr\kern
0.80002pt$\hss\leavevmode\resizebox{2.68205pt}{2.72223pt}{\rotatebox[origin={c}]{90.0}{(}}\hss$\crcr\nointerlineskip\cr$\hss\scriptstyle
r\hss$\crcr}}}\limits}{\mathop{\vbox{\halign{#\cr\kern
0.80002pt$\hss\leavevmode\resizebox{1.91574pt}{1.94444pt}{\rotatebox[origin={c}]{90.0}{(}}\hss$\crcr\nointerlineskip\cr$\hss\scriptscriptstyle
r\hss$\crcr}}}\limits})^{-}\left(b\downarrow_{\sqsubseteq^{\prime}}c\right)$.

Conversely, let $r$ be a formal topology map from
$(S,\mathrel{\blacktriangleleft}_{\sqsubset},\sqsubseteq)$ to
${(S^{\prime},\mathrel{\blacktriangleleft}^{\prime}_{\sqsubset^{\prime}},\sqsubseteq^{\prime})}$.
We must show that $r^{\ddagger}$ given by (4.15) satisfies 2f and 2g.

2f Let $a\sqsubset a^{\prime}$. Since
$S\mathrel{\blacktriangleleft}_{\sqsubset}r^{-}S^{\prime}$ by 1, there exists
$A\in\mathsf{Fin}(r^{-}S^{\prime})$ such that
$a\ll_{\mathrel{\blacktriangleleft}}A$, so there exist
$A^{\prime}\sqsubset_{L}A$ and $B\in\mathsf{Fin}(S^{\prime})$ such that
$a\mathrel{\blacktriangleleft}A^{\prime}$ and $A\mathrel{r_{L}}B$. Then
$A^{\prime}\mathrel{(r^{\ddagger})_{L}}B$.

2g Suppose $a\sqsubset a^{\prime}\mathrel{r^{\ddagger}}b$ and
$a^{\prime}\mathrel{r^{\ddagger}}c$. Then,
$a^{\prime}\mathrel{\blacktriangleleft}_{\sqsubset}r^{-}b$ and
$a^{\prime}\mathrel{\blacktriangleleft}_{\sqsubset}r^{-}c$. Since
$b\mathrel{\blacktriangleleft}^{\prime}_{\sqsubset^{\prime}}\mathord{\downarrow}_{\sqsubset^{\prime}}b$
and
$c\mathrel{\blacktriangleleft}^{\prime}_{\sqsubset^{\prime}}\mathord{\downarrow}_{\sqsubset^{\prime}}c$,
we have
$a^{\prime}\mathrel{\blacktriangleleft}_{\sqsubset}r^{-}\mathord{\downarrow}_{\sqsubset^{\prime}}b$
and
$a^{\prime}\mathrel{\blacktriangleleft}_{\sqsubset}r^{-}\mathord{\downarrow}_{\sqsubset^{\prime}}c$
by 2. Then, by ($\mathord{\downarrow}$-right) and 2, we have
$a^{\prime}\mathrel{\blacktriangleleft}_{\sqsubset}r^{-}\left(\left(\mathord{\downarrow}_{\sqsubset^{\prime}}b\right)\mathord{\downarrow}_{\sqsubseteq^{\prime}}\left(\mathord{\downarrow}_{\sqsubset^{\prime}}c\right)\right)\subseteq
r^{-}\left(b\downarrow_{\sqsubset^{\prime}}c\right)$. Thus, there exists
$A\in\mathsf{Fin}(r^{-}\left(b\downarrow_{\sqsubset^{\prime}}c\right))$ such
that $a\ll_{\mathrel{\blacktriangleleft}}A$. Then, as in the proof of 2f
above, we find $D\in\mathsf{Fin}(b\downarrow_{\sqsubset^{\prime}}c)$ and
$A^{\prime}\in\mathsf{Fin}(S)$ such that
$a\mathrel{\blacktriangleleft}A^{\prime}$ and
$A^{\prime}\mathrel{(r^{\ddagger})_{L}}D$. ∎

Let $\mathsf{ContBCov}$ be the full subcategory of $\mathsf{BCov}$ consisting
of continuous basic covers, and let $\mathsf{LKFTop}$ be the full subcategory
of $\mathsf{FTop}$ consisting of locally compact formal topologies. Then, it
is straightforward to show that the composition of the assignments $r\mapsto
r^{\dagger}$ and $r\mapsto\mathchoice{\mathop{\vbox{\halign{#\cr\kern
0.80002pt$\hss\leavevmode\resizebox{3.8315pt}{3.8889pt}{\rotatebox[origin={c}]{90.0}{(}}\hss$\crcr\nointerlineskip\cr$\hss\displaystyle
r\hss$\crcr}}}\limits}{\mathop{\vbox{\halign{#\cr\kern
0.80002pt$\hss\leavevmode\resizebox{3.8315pt}{3.8889pt}{\rotatebox[origin={c}]{90.0}{(}}\hss$\crcr\nointerlineskip\cr$\hss\textstyle
r\hss$\crcr}}}\limits}{\mathop{\vbox{\halign{#\cr\kern
0.80002pt$\hss\leavevmode\resizebox{2.68205pt}{2.72223pt}{\rotatebox[origin={c}]{90.0}{(}}\hss$\crcr\nointerlineskip\cr$\hss\scriptstyle
r\hss$\crcr}}}\limits}{\mathop{\vbox{\halign{#\cr\kern
0.80002pt$\hss\leavevmode\resizebox{1.91574pt}{1.94444pt}{\rotatebox[origin={c}]{90.0}{(}}\hss$\crcr\nointerlineskip\cr$\hss\scriptscriptstyle
r\hss$\crcr}}}\limits}$ given by (4.12) and (4.14), respectively, determines a
functor $F\colon\mathsf{SContFCov}\to\mathsf{ContBCov}$. By Proposition 4.5,
$F$ is full and faithful, and it restricts to a full and faithful functor from
$\mathsf{LSContFCov}$ to $\mathsf{LKFTop}$.

######  Theorem .

$\mathsf{SContFCov}$ is equivalent to $\mathsf{ContBCov}$. The equivalence
restricts to an equivalence between $\mathsf{LSContFCov}$ and
$\mathsf{LKFTop}$.

###### Proof.

First, we show that the functor
$F\colon\mathsf{SContFCov}\to\mathsf{ContBCov}$ described above is essentially
surjective. Let $(S,\mathrel{\lhd})$ be a continuous basic cover with a
relation $\mathsf{wb}\subseteq S\times S$ satisfying (4.10). Define a finitary
cover ${\mathrel{\blacktriangleleft}}$ on $\mathsf{Fin}(S)$ by

$\displaystyle
A\mathrel{\mathrel{\blacktriangleleft}}\mathcal{U}\stackrel{{\scriptstyle\textup{def}}}{{\iff}}A\mathrel{\lhd}\bigcup\mathcal{U}.$
(4.17) Then, define a relation $\sqsubset$ on $\mathsf{Fin}(S)$ by
$\displaystyle A\sqsubset
B\stackrel{{\scriptstyle\textup{def}}}{{\iff}}\exists
C\in\mathsf{Fin}(S)\left(A\mathrel{\lhd}C\mathrel{\mathsf{wb}_{L}}B\right).$
(4.18)

One can easily show that $\sqsubset$ is idempotent by noting that
$a\mathrel{\lhd}\mathsf{wb}^{-}a\mathrel{\lhd}\left\\{a\right\\}$. We show
that $(\mathsf{Fin}(S),\mathrel{\blacktriangleleft},\sqsubset)$ satisfies
(4.6). First, suppose $A\sqsubset B\mathrel{\blacktriangleleft}\mathcal{U}$.
Then, there exists $C\in\mathsf{Fin}(S)$ such that
$A\mathrel{\lhd}C\mathrel{\mathsf{wb}_{L}}B$. Since
$B\mathrel{\lhd}\mathsf{wb}^{-}\bigcup\mathcal{U}$, there exists
$D\in\mathsf{Fin}(\mathsf{wb}^{-}\bigcup\mathcal{U})$ such that
$C\mathrel{\lhd}D$. Then, there exists
$\mathcal{V}\in\mathsf{Fin}(\mathsf{Fin}(S))$ such that $D=\bigcup\mathcal{V}$
and $\mathcal{V}\mathrel{(\mathsf{wb}_{L})_{L}}\mathcal{U}$. Thus
$A\mathrel{\mathrel{\blacktriangleleft}}\mathcal{V}\sqsubset_{L}\mathcal{U}$.
Conversely, if
$A\mathrel{\mathrel{\blacktriangleleft}}\mathcal{V}\sqsubset_{L}\mathcal{U}$,
then
$A\sqsubset\bigcup\mathcal{U}\mathrel{\mathrel{\blacktriangleleft}}\mathcal{U}$.
Therefore, $(\mathsf{Fin}(S),\mathrel{\blacktriangleleft},\sqsubset)$ is a
strong continuous finitary cover.

It is straightforward to show that $(S,\mathrel{\lhd})$ is isomorphic to the
basic cover $(\mathsf{Fin}(S),\mathrel{\blacktriangleleft}_{\sqsubset})$
determined by $(\mathsf{Fin}(S),\mathrel{\blacktriangleleft},\sqsubset)$ as in
(4.11). Specifically, we have an isomorphism
$r\colon(S,\mathrel{\lhd})\to(\mathsf{Fin}(S),\mathrel{\blacktriangleleft}_{\sqsubset})$
defined by

$a\mathrel{r}A\stackrel{{\scriptstyle\textup{def}}}{{\iff}}a\mathrel{\lhd}A$

with an inverse
$s\colon(\mathsf{Fin}(S),\mathrel{\blacktriangleleft}_{\sqsubset})\to(S,\mathrel{\lhd})$
defined by

$A\mathrel{s}a\stackrel{{\scriptstyle\textup{def}}}{{\iff}}A\mathrel{\lhd}\left\\{a\right\\}.$

Hence, the functor $F\colon\mathsf{SContFCov}\to\mathsf{ContBCov}$ is
essentially surjective.

Next, we show that for any locally compact formal topology
$(S,\mathrel{\lhd},\leq)$ equipped with a relation $\mathsf{wb}$ satisfying
(4.10), the strong continuous finitary cover
${(\mathsf{Fin}(S),\mathrel{\blacktriangleleft},\sqsubset)}$ defined by (4.17)
and (4.18) is localized. Suppose $A\sqsubset
B\mathrel{\blacktriangleleft}\mathcal{U}$. Then
$B\mathrel{\lhd}\mathsf{wb}^{-}\bigcup\mathcal{U}\downarrow_{\leq}\mathsf{wb}^{-}B$,
so there exists
$C\in\mathsf{Fin}(\mathsf{wb}^{-}\bigcup\mathcal{U}\downarrow_{\leq}\mathsf{wb}^{-}B)$
such that $A\mathrel{\lhd}C$. Thus, there exists
$\mathcal{V}\in\mathsf{Fin}(\mathsf{Fin}(S))$ such that
$C=\bigcup{\mathcal{V}}$, $\mathcal{V}\sqsubset_{L}\mathcal{U}$, and
$\mathcal{V}\sqsubset_{L}\left\\{B\right\\}$. Hence
$A\mathrel{\blacktriangleleft}\mathcal{V}\in\mathsf{Fin}(B\downarrow_{\sqsubset}\mathcal{U})$,
and so $(\mathsf{Fin}(S),\mathrel{\blacktriangleleft},\sqsubset)$ is
localized.

As we have shown in the first part, as a basic cover,
$(S,\mathrel{\lhd},\leq)$ is isomorphic to the locally compact formal topology
$(\mathsf{Fin}(S),\mathrel{\blacktriangleleft}_{\sqsubset},\sqsubseteq)$
determined by ${(\mathsf{Fin}(S),\mathrel{\blacktriangleleft},\sqsubset)}$.
Since any isomorphism between the underlying basic covers is a formal topology
map [CMS13, Proposition 5.6], the restriction of
$F\colon\mathsf{SContFCov}\to\mathsf{ContBCov}$ to $\mathsf{LSContFCov}$ and
$\mathsf{LKFTop}$ is essentially surjective. ∎

## Acknowledgements

We thank the following people: anonymous referees for many useful suggestions;
Steve Vickers for valuable feedback on a preliminary version of the paper;
Francesco Ciraulo, Milly Maietti, and Giovanni Sambin for illuminating
discussions on the predicativity problem of locally compact formal topologies.

## References

  * [AJ94] Samson Abramsky and Achim Jung.  Domain theory.  In Handbook of Logic in Computer Science, volume 3, pages 1–168. Oxford University Press, 1994.
  * [AR10] Peter Aczel and Michael Rathjen.  CST Book draft.  http://www1.maths.leeds.ac.uk/˜rathjen/book.pdf, August 2010.
  * [Bec69] Jonathan Mock Beck.  Distributive laws.  In B. Eckmann, editor, Seminar on Triples and Categorical Homology Theory, volume 80 of Lecture Notes in Math., pages 119–140. Springer, Berlin, Heidelberg, 1969.
  * [Bis67] Errett Bishop.  Foundations of Constructive Analysis.  McGraw-Hill, New York, 1967.
  * [CMS13] Francesco Ciraulo, Maria Emilia Maietti, and Giovanni Sambin.  Convergence in formal topology: a unifying notion.  J. Log. Anal., 5(2):1–45, 2013.
  * [CZ03] Thierry Coquand and Guo-Qiang Zhang.  A representation of stably compact spaces, and patch topology.  Theoret. Comput. Sci., 305(1-3):77–84, 2003.
  * [Esc98] Martín Hötzel Escardó.  Properly injective spaces and function spaces.  Topology Appl., 89(1):75–120, 1998.
  * [Fre64] Peter J. Freyd.  Abelian Categories: An Introduction to the Theory of Functors.  Harper’s Series of in Modern Mathematics. Haper & Row, 1964.
  * [GHK+03] Gerhard Gierz, Karl Heinrich Hofmann, Klaus Keimel, Jimmie D. Lawson, Michael Mislove, and Dana S. Scott.  Continuous Lattices and Domains.  Cambridge University Press, 2003.
  * [JKM99] Achim Jung, Mathias Kegelmann, and M. Andrew Moshier.  Multi lingual sequent calculus and coherent spaces.  Fund. Inform., 37(4):369–412, 1999.
  * [Joh82] Peter T. Johnstone.  Stone Spaces.  Cambridge University Press, 1982.
  * [Joh02] Peter T. Johnstone.  Sketches of an elephant: a topos theory compendium. Vol. 2, volume 44 of Oxford Logic Guides.  Oxford University Press, 2002.
  * [JS96] Achim Jung and Philipp Sünderhauf.  On the duality of compact vs. open.  Ann. N. Y. Acad. Sci., 806(1):214–230, 1996.
  * [Kaw20] Tatsuji Kawai.  Presenting de Groot duality of stably compact spaces.  Theoret. Comput. Sci., 823:44–68, 2020.
  * [Koc95] Anders Kock.  Monads for which structures are adjoint to units.  J. Pure. Appl. Algebra, 104(1):41–59, 1995.
  * [Mac98] Saunders Mac Lane.  Categories for the Working Mathematician, volume 5 of Graduate Texts in Mathematics.  Springer-Verlag, New York, second edition, 1998.
  * [ML84] Per Martin-Löf.  Intuitionistic type theory.  Bibliopolis, Napoli, 1984.
  * [Neg98] Sara Negri.  Continuous lattices in formal topology.  In Eduardo Giménez and Christine Paulin-Mohring, editors, Types for Proofs and Programs. TYPES 1996, volume 1512 of Lecture Notes in Comput. Sci., pages 333–353. Springer, Berlin, Heidelberg, 1998.
  * [Neg02] Sara Negri.  Continuous domains as formal spaces.  Math. Structures Comput. Sci., 12(1):19–52, 2002.
  * [RSW18] Davide Rinaldi, Peter Schuster, and Daniel Wessel.  Eliminating disjunctions by disjunction elimination.  Indagationes Mathematicae, 29(1):226–259, 2018.
  * [Sam87] Giovanni Sambin.  Intuitionistic formal spaces—a first communication.  In Dimiter G. Skordev, editor, Mathematical Logic and its Applications, volume 305, pages 187–204. Plenum Press, New York, 1987.
  * [Sch93] Andrea Schalk.  Algebras for generalized power constructions.  PhD thesis, Technische Universität Darmstadt, 1993.
  * [Sco72] Dana Scott.  Continuous lattices.  In F. William Lawvere, editor, Toposes, Algebraic Geometry and Logic, volume 274 of Lecture Notes in Math., pages 97–136. Springer, Berlin, Heidelberg, 1972.
  * [Smy77] Michael. B. Smyth.  Effectively given domains.  Theoret. Comput. Sci., 5:257–274, 1977.
  * [Smy92] Michael. B. Smyth.  Stable compactification. I.  J. London Math. Soc. (2), 45(2):321–340, 1992.
  * [van12] Sam J. van Gool.  Duality and canonical extensions for stably compact spaces.  Topology Appl., 159(1):341–359, 2012.
  * [Vic89] Steven Vickers.  Topology via Logic.  Cambridge University Press, 1989.
  * [Vic93] Steven Vickers.  Information systems for continuous posets.  Theoret. Comput. Sci., 114:201–229, 1993.
  * [Vic04a] Steven Vickers.  The double powerlocale and exponentiation: A case study in geometric reasoning.  Theory Appl. Categ., 12(13):372–422, 2004.
  * [Vic04b] Steven Vickers.  Entailment systems for stably locally compact locales.  Theoret. Comput. Sci., 316(1):259–296, 2004.