connectedComponent_eq — Mathlib

English

If y ∈ connectedComponent x, then connectedComponent x = connectedComponent y.

Русский

Если y ∈ connectedComponent x, то connectedComponent x = connectedComponent y.

LaTeX

$$$y \in connectedComponent x \Rightarrow connectedComponent x = connectedComponent y$$$

Lean4

theorem connectedComponent_eq {x y : α} (h : y ∈ connectedComponent x) : connectedComponent x = connectedComponent y :=
  eq_of_subset_of_subset (isConnected_connectedComponent.subset_connectedComponent h)
    (isConnected_connectedComponent.subset_connectedComponent
      (Set.mem_of_mem_of_subset mem_connectedComponent (isConnected_connectedComponent.subset_connectedComponent h)))

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