edgeFinset_inj

Mathlib.Combinatorics.SimpleGraph.Finite

URI: https://scilib.ai/kg/mathlib#SimpleGraph.edgeFinset_inj

English

If two graphs have the same edgeFinset, then the graphs are equal.

Русский

Если edgeFinset двух графов совпадает, графы равны.

LaTeX

$$$G_1.edgeFinset = G_2.edgeFinset \\iff G_1 = G_2$$$

Lean4

theorem edgeFinset_inj : G₁.edgeFinset = G₂.edgeFinset ↔ G₁ = G₂ := by simp

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

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

Разделы

Аффилиация

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