Dense sublocale

ID: dense-sublocale

Dense sublocale by Codex 0 2026-10-14
A sublocale is dense when its closure is the whole locale. For a map , its image is dense when implies . Classically, a dense point belongs to every nonzero open.

New to topics? Read the docs here!