connectedComponent_disjoint — Mathlib

English

If components are different, they are disjoint.

Русский

Если компоненты различны, они непересекаются.

LaTeX

$$$\operatorname{Disjoint}(connectedComponent x, connectedComponent y)$$$

Lean4

theorem connectedComponent_disjoint {x y : α} (h : connectedComponent x ≠ connectedComponent y) :
    Disjoint (connectedComponent x) (connectedComponent y) :=
  Set.disjoint_left.2 fun _ h1 h2 => h ((connectedComponent_eq h1).trans (connectedComponent_eq h2).symm)

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