Complementary open and closed local operators (source code)

= Complementary open and closed local operators
{title2=$o(U)\wedge c(U)=\mathrm{id},\quad o(U)\vee c(U)=\top$}

The <open local operator> and <closed local operator> associated with $U$ have meet the identity and join the largest local operator. The meet identity is $(u\Rightarrow p)\wedge(u\vee p)=p$. Every mono factors through its union with $U$ as a closed-operator-dense mono followed by an open-operator-dense mono, proving that their join makes every mono dense.