English
In a PreirreducibleSpace X, any nonempty open subset s is dense in X provided X is Preirreducible.
Русский
В преднеразложимом пространстве X любое непустое открытое множество s плотно в X, если X является преднеразложимым пространством.
LaTeX
$$$\\text{dense}(s) \\text{ for all } s \\text{ open}, s \\neq \\emptyset \\text{ in a PreirreducibleSpace } X$$$
Lean4
/-- In a (pre)irreducible space, a nonempty open set is dense. -/
protected theorem dense [PreirreducibleSpace X] (ho : IsOpen s) (hne : s.Nonempty) : Dense s :=
dense_iff_inter_open.2 fun _t hto htne => nonempty_preirreducible_inter hto ho htne hne
