English
A set s is totally disconnected if every subset t ⊆ s that is preconnected is a subsingleton.
Русский
Множество s называется абсолютно разобщённым, если каждая его предсвязанная подмножество является либо пустым, либо одиночкой.
LaTeX
$$IsTotallyDisconnected(s) := ∀ t, t ⊆ s → IsPreconnected t → t.Subsingleton$$
Lean4
/-- A set `s` is called totally disconnected if every subset `t ⊆ s` which is preconnected is
a subsingleton, i.e. either empty or a singleton. -/
def IsTotallyDisconnected (s : Set α) : Prop :=
∀ t, t ⊆ s → IsPreconnected t → t.Subsingleton