Positive open of a locale
ID: positive-open-of-a-locale
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.
New to topics? Read the docs here!