connectedComponent_eq_iff_mem — Mathlib

English

The equality of connected components holds iff one contains the other’s point.

Русский

Равенство связанных компонент эквивалентно тому, что точка одного множества принадлежит другой компоненте.

LaTeX

$$$connectedComponent x = connectedComponent y \iff x \in connectedComponent y$$$

Lean4

theorem connectedComponent_eq_iff_mem {x y : α} :
    connectedComponent x = connectedComponent y ↔ x ∈ connectedComponent y :=
  ⟨fun h => h ▸ mem_connectedComponent, fun h => (connectedComponent_eq h).symm⟩

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