biUnion_connectedComponent_eq — Mathlib

English

For a subset u of X, if the preimage of u via the inclusion into X is clopen and u ⊆ v, then u equals the union over x ∈ u of connectedComponentIn v x.

Русский

Для множества u ⊆ X, если предобраз через включение в X clopen и u ⊆ v, то u есть объединение по x∈u connectedComponentIn v x.

LaTeX

$$$IsClopen(\,Set.preimage(Subtype.val, u)\,) \land (u \subseteq v) \Rightarrow u = \bigcup_{x\in u} connectedComponentIn v x$$$

Lean4

/-- A clopen set is the union of its connected components. -/
theorem biUnion_connectedComponent_eq {Z : Set α} (h : IsClopen Z) : ⋃ x ∈ Z, connectedComponent x = Z :=
  Subset.antisymm (iUnion₂_subset fun _ => h.connectedComponent_subset) fun _ h =>
    mem_iUnion₂_of_mem h mem_connectedComponent

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