IsTotallyDisconnected — Mathlib

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

Похожие утверждения