IsConnected — Mathlib

English

A set S is connected if it is nonempty and preconnected.

Русский

Множество S связано, если оно непусто и предсоединено.

LaTeX

$$$$ \\operatorname{IsConnected}(S) \\;\\Longleftrightarrow\\; S \\neq \\varnothing \\wedge \\operatorname{IsPreconnected}(S). $$$$

Lean4

/-- A connected set is one that is nonempty and where there is no non-trivial open partition. -/
def IsConnected (s : Set α) : Prop :=
  s.Nonempty ∧ IsPreconnected s

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