Corollary. Properties of \sqcup [dt-0018]
When lubs exist, the binary \sqcup operator is idempotent, commutative, and associative. Also, we have that x \sqsubseteq y iff x \sqcup y = y.
When lubs exist, the binary \sqcup operator is idempotent, commutative, and associative. Also, we have that x \sqsubseteq y iff x \sqcup y = y.