English
Let s be a subset of a topological space X. Then s is irreducible if and only if s is nonempty and s is preirreducible; equivalently, there are no nontrivial disjoint open subsets of s whose union is s.
Русский
Пусть s ⊆ X, где X — топологическое пространство. Подмножество s называется неразложимым тогда и только тогда, когда оно непусто и оно преднеразложимо; эквивалентно: не существует пары непустых непересекающихся открытых подмножеств внутри s, чьи объединения дают s.
LaTeX
$$$\\operatorname{IsIrreducible}(s) \\iff s \\neq \\emptyset \\wedge \\operatorname{IsPreirreducible}(s)$$$
Lean4
/-- An irreducible set `s` is one that is nonempty and
where there is no non-trivial pair of disjoint opens on `s`. -/
@[stacks 004V "(1) as predicate on subsets of a space"]
def IsIrreducible (s : Set X) : Prop :=
s.Nonempty ∧ IsPreirreducible s
