connectedComponent_subset_iInter_isClopen

English

A clopen set Z is the union of its connected components; i.e., Z equals the union over x in Z of connectedComponent x.

Русский

Замкнутое и открытое множество Z является объединением своих связных компонент: Z = ⋃_{x∈Z} connectedComponent x.

LaTeX

$$$Z\ text{ IsClopen } \Rightarrow \bigcup_{x\in Z} connectedComponent x = Z$$$

Lean4

/-- The connected component of a point is always a subset of the intersection of all its clopen
neighbourhoods. -/
theorem connectedComponent_subset_iInter_isClopen {x : α} :
    connectedComponent x ⊆ ⋂ Z : { Z : Set α // IsClopen Z ∧ x ∈ Z }, Z :=
  subset_iInter fun Z => Z.2.1.connectedComponent_subset Z.2.2

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