English
A set s is preirreducible if there are no two disjoint open sets on s whose intersections with s are both nonempty, i.e., s cannot be split into two nontrivial open pieces.
Русский
Множество s преднеразделимо, если не существует пары непересекающихся открытых множеств на s, чьи пересечения с s непусты.
LaTeX
$$$\\text{IsPreirreducible}(s) := ∀ u v,\\ IsOpen(u) ∧ IsOpen(v) \\Rightarrow (s\\cap u)\\neq\\varnothing ∧ (s\\cap v)\\neq \\varnothing \\Rightarrow (s\\cap (u\\cap v))\\neq \\varnothing$$$
Lean4
/-- A preirreducible set `s` is one where there is no non-trivial pair of disjoint opens on `s`. -/
def IsPreirreducible (s : Set X) : Prop :=
∀ u v : Set X, IsOpen u → IsOpen v → (s ∩ u).Nonempty → (s ∩ v).Nonempty → (s ∩ (u ∩ v)).Nonempty
