Lim-inf convergence

The lim-inf convergence of a lattice $L$ is a Moore-Smith convergence class of nets on $L$. It is based on the operation $\mathop{\underline\lim}N$ - the lower limit of a net $N$ (see lim_inf in [W11]):

$\mathop{\underline\lim}N = \sup_{i} \inf_{j\geq i} N(j)$

Namely, nets in the lim-inf convergence satisfy the condition that all their subnets have the same lower limit which is the convergence point (see [W28]). A subnet is embeddable in and cofinal with a net after this embedding.

 definition
   let L be non empty RelStr;
   func lim_inf-Convergence L -> Convergence-Class of L means
     for N being net of L st N in NetUniv L
     for x being Element of the carrier of L holds
      [N,x] in it iff for M being subnet of N holds x = lim_inf M;
 end;

We may also characterize the lim-inf convergence by the other equivalent conditions:

• $\inf_{k} M(k) \leq \mathop{\underline\lim}N$ for all subnets $M$ of $N$, and
• $\inf_{i} (N(p(i))) \leq \mathop{\underline\lim}N$ for all non-descending automorphisms $p$ of indices of $N$ (i.e., automorphisms $p$ such that for any index $i$, $p(i) \geq i$).

The lim-inf convergence induces a topology on the lattice $L$ in the standard way. The topology induced is the family of all subsets $A$ of $L$ which meet the following condition: for every net $N$ and its convergent point $x$ from lim-inf convergence in $L$, if $x$ belongs to $A$, then $N$ is eventually in $A$. For details, see [Y6].

By a top-lattice we mean a lattice equipped with a topology. If the topology is induced by the lim-inf convergence of the lattice part of the top-lattice, we call such a top-lattice a lim-inf top-lattice. Moreover, if the lattice part of it is complete, we will call it a complete lim-inf top-lattice.