connectedComponentIn_univ — Mathlib

English

The component in the universal set equals the connected component.

Русский

Компонента внутри множества единиц равна связной компоненте.

LaTeX

$$$connectedComponentIn \operatorname{univ} x = connectedComponent x$$$

Lean4

theorem connectedComponentIn_univ (x : α) : connectedComponentIn univ x = connectedComponent x :=
  subset_antisymm (isPreconnected_connectedComponentIn.subset_connectedComponent <| mem_connectedComponentIn trivial)
    (isPreconnected_connectedComponent.subset_connectedComponentIn mem_connectedComponent <| subset_univ _)

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