eq_of_common_vertex — Mathlib

English

If a vertex lies in the supports of two connected components, then the two components are equal.

Русский

Если вершина лежит в опорах двух компонент связности, то эти компоненты равны.

LaTeX

$$$\\\\forall {v} : V\\\\, {c c' : G.ConnectedComponent}, (v \\\\in c.supp) \\\\land (v \\\\in c'.supp) \\\\Rightarrow c = c'$$$

Lean4

theorem eq_of_common_vertex {v : V} {c c' : ConnectedComponent G} (hc : v ∈ c.supp) (hc' : v ∈ c'.supp) : c = c' :=
  by
  simp only [mem_supp_iff] at *
  rw [← hc, ← hc']

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