supp_inj

Mathlib.Combinatorics.SimpleGraph.Ends.Defs

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

English

Equivalence between equality of supports and equality of components.

Русский

Эквивалентность: равенство поддержек эквивалентно равенству компонент.

LaTeX

$$$$ \mathrm{ComponentCompl.supp\,injection}.eq_iff $$$$

Lean4

theorem supp_inj {C D : G.ComponentCompl K} : C.supp = D.supp ↔ C = D :=
  ComponentCompl.supp_injective.eq_iff

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

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

Разделы

Аффилиация

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