English
Let S be a subset of a topological space. S is preconnected if it cannot be separated by an open partition: whenever S lies inside the union of two open sets U and V, and S meets both U and V, then S meets U ∩ V.
Русский
Пусть S — подмножество топологического пространства. S называется предсоединённым, если его нельзя разложить на две открытые части: если S ⊆ U ∪ V для открытых U,V и S пересекает каждое из них, то S пересекает и их пересечение U ∩ V.
LaTeX
$$$$ \\operatorname{IsPreconnected}(S) \\;\\Longleftrightarrow\\; \\forall U,V,\\ \\text{IsOpen}(U) \\wedge \\text{IsOpen}(V) \\rightarrow S \\subseteq U \\cup V \\rightarrow (S \\cap U) \\neq \\varnothing \\rightarrow (S \\cap V) \\neq \\varnothing \\rightarrow (S \\cap (U \\cap V)) \\neq \\varnothing.$$$$
Lean4
/-- A preconnected set is one where there is no non-trivial open partition. -/
def IsPreconnected (s : Set α) : Prop :=
∀ u v : Set α, IsOpen u → IsOpen v → s ⊆ u ∪ v → (s ∩ u).Nonempty → (s ∩ v).Nonempty → (s ∩ (u ∩ v)).Nonempty
