irreducibleComponent_subset_connectedComponent

English

Every irreducible component is contained in the connected component of its point.

Русский

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

LaTeX

$$$\text{irreducibleComponent}(x) \subseteq \operatorname{connectedComponent}(x)$$$

Lean4

theorem irreducibleComponent_subset_connectedComponent {x : α} : irreducibleComponent x ⊆ connectedComponent x :=
  isIrreducible_irreducibleComponent.isConnected.subset_connectedComponent mem_irreducibleComponent

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