supp_inj

Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected

URI: https://scilib.ai/kg/mathlib#SimpleGraph.ConnectedComponent.supp_inj

English

Two connected components have the same support if and only if they are equal.

Русский

Две компоненты связности имеют одинаковую опору тогда и только тогда, когда они равны.

LaTeX

$$$C.supp = D.supp \\\\iff C = D$$$

Lean4

@[simp]
theorem supp_inj {C D : G.ConnectedComponent} : C.supp = D.supp ↔ C = D :=
  ConnectedComponent.supp_injective.eq_iff

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru