Positive open of a locale
= Positive open of a locale
{title2=$\operatorname{Pos}(a)$}
= Positive opens of a locale
{synonym}
An open is positive when its positivity truth value holds. Positivity gives a constructive witness of inhabitedness and must not be replaced by double-negated nonemptiness.