Infimum of Intersection of Upper Closures equals Join Operands
Jump to navigation
Jump to search
Theorem
Let $L = \struct {S, \vee, \preceq}$ be a join semilattice.
Let $x, y \in S$.
Then $\map \inf {x^\succeq \cap y^\succeq} = x \vee y$
Proof
By Intersection of Upper Closures is Upper Closure of Join Operands:
- $x^\succeq \cap y^\succeq = \paren {x \vee y}^\succeq$
Thus by Infimum of Upper Closure of Element:
- $\map \inf {x^\succeq \cap y^\succeq} = x \vee y$
$\blacksquare$
Sources
- Mizar article WAYBEL16:1