mem_connectedComponent — Mathlib

English

Let α be a topological space and x ∈ α. Then x lies in the connected component of x.

Русский

Пусть α — топологическое пространство и x ∈ α. Тогда x принадлежит связной компоненте x.

LaTeX

$$$x \in \operatorname{connectedComponent}(x)$$$

Lean4

theorem mem_connectedComponent {x : α} : x ∈ connectedComponent x :=
  mem_sUnion_of_mem (mem_singleton x) ⟨isPreconnected_singleton, mem_singleton x⟩

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