PhyslibAlpha.Mathematics.Order.VectorLattice

Let $G$ be a vector lattice. For any elements $y, z \in G$, if $y \le z$ and $z \ge 0$, then the positive part of $y$, denoted by $y^+$, satisfies $y^+ \le z$.

In a real vector lattice $G$, let $f_1, f_2, g$ be elements such that $f_1 \ge 0$, $f_2 \ge 0$, and $0 \le g \le f_1 + f_2$. Then the elements $g \sqcap f_1$ and $g - (g \sqcap f_1)$ satisfy $0 \le g \sqcap f_1 \le f_1$ and $0 \le g - (g \sqcap f_1) \le f_2$, where $\sqcap$ denotes the infimum (greatest lower bound) of two elements.

Let $G$ be a real vector lattice. For any elements $h_1, h_2, c \in G$ such that $h_1 \ge 0$, $h_2 \ge 0$, and $c \ge 0$, the infimum of the sum $h_1 + h_2$ with $c$ is less than or equal to the sum of the individual infima of $h_1$ and $h_2$ with $c$: $$(h_1 + h_2) \sqcap c \le (h_1 \sqcap c) + (h_2 \sqcap c)$$ where $\sqcap$ denotes the infimum (greatest lower bound) of two elements.

Let $G$ be a real vector lattice. For any nonnegative elements $x, u, v \in G$, if $u$ and $v$ are disjoint (that is, their infimum $u \sqcap v = 0$), then the infimum of $x$ with the sum $u + v$ is equal to the sum of the individual infima: $$x \sqcap (u + v) = (x \sqcap u) + (x \sqcap v)$$

Let $x, u,$ and $v$ be non-negative elements in a vector lattice. If $x$ is disjoint from $u$ (i.e., $x \sqcap u = 0$) and $x$ is disjoint from $v$ (i.e., $x \sqcap v = 0$), then $x$ is disjoint from their sum, such that $x \sqcap (u + v) = 0$.

Let $G$ be a vector lattice and $x \in G$ be a non-negative element ($x \geq 0$). For any finite family of non-negative elements $\{u_i\}_{i \in s}$ in $G$, if $x$ is disjoint from every $u_i$ (i.e., $x \sqcap u_i = 0$ for all $i \in s$), then $x$ is disjoint from their sum: $$x \sqcap \sum_{i \in s} u_i = 0$$

Let $G$ be a vector lattice, and let $x, w, s \in G$ be non-negative elements. If $w$ and $s$ are disjoint, meaning their infimum is zero ($w \wedge s = 0$), then the infimum of $x + w$ and $s$ is less than or equal to the infimum of $x$ and $s$: $$(x + w) \wedge s \le x \wedge s$$

Let $G$ be a vector lattice. Let $x \in G$ be a nonnegative element ($x \geq 0$) and $\{u_i\}_{i \in t}$ be a finite family of pairwise disjoint nonnegative elements, meaning $u_i \geq 0$ for all $i \in t$ and $u_i \sqcap u_j = 0$ for all $i, j \in t$ such that $i \neq j$. Then the infimum of $x$ with the sum of the family is equal to the sum of the individual infima: $$x \sqcap \sum_{i \in t} u_i = \sum_{i \in t} (x \sqcap u_i)$$ where $\sqcap$ denotes the infimum operation.

In a real vector lattice $G$, let $(a_n)_{n \in \mathbb{N}}$ be a sequence in $G$ and let $c \in G$ be its least upper bound. For any element $b \in G$, the least upper bound of the sequence $(a_n \sqcap b)_{n \in \mathbb{N}}$ is given by $c \sqcap b$. That is, $\sup_{n \in \mathbb{N}} (a_n \sqcap b) = (\sup_{n \in \mathbb{N}} a_n) \sqcap b$, where $\sqcap$ denotes the infimum (meet) of two elements.

Let $G$ be a real vector lattice. For any non-negative real number $c \geq 0$ and any elements $x, y \in G$, the scalar multiplication by $c$ distributes over the infimum (meet) of $x$ and $y$, such that $c \cdot (x \sqcap y) = (c \cdot x) \sqcap (c \cdot y)$.

Let $G$ be a real vector lattice. For any nonnegative elements $g, u \in G$ (where $0 \le g$ and $0 \le u$) that are disjoint, meaning their infimum $g \sqcap u = 0$, and for any nonnegative real scalar $a \ge 0$, the element $g$ and the scaled element $a \cdot u$ remain disjoint, such that $g \sqcap (a \cdot u) = 0$.

Let $G$ be a real vector lattice. For any non-negative elements $u, v \in G$ that are disjoint (meaning their infimum $u \sqcap v = 0$), and for any non-negative real scalars $a, b \ge 0$, the scaled elements $a \cdot u$ and $b \cdot v$ remain disjoint, such that $a \cdot u \sqcap b \cdot v = 0$.

Let $G$ be a real vector lattice. Let $(a_n)_{n \in \mathbb{N}}$ be a sequence in $G$ and $c \in G$ be its least upper bound (supremum). For any strictly positive real scalar $r > 0$, the element $r \cdot c$ is the least upper bound of the scaled sequence $(r \cdot a_n)_{n \in \mathbb{N}}$. That is, if $c = \sup_{n} a_n$, then $r \cdot c = \sup_{n} (r \cdot a_n)$.