subset_connectedComponent — Mathlib

English

If a set is connected, it is contained in the connected component of any of its points.

Русский

Если множество связано, то оно содержится в связной компоненте любой своей точки.

LaTeX

$$$s \subseteq connectedComponent x \quad\text{whenever } x \in s \text{ and } IsConnected s$$$

Lean4

theorem subset_connectedComponent {x : α} {s : Set α} (H1 : IsConnected s) (H2 : x ∈ s) : s ⊆ connectedComponent x :=
  H1.2.subset_connectedComponent H2

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