edgeSet_injective

Mathlib.Combinatorics.SimpleGraph.Basic

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

English

The edge set map is injective: if E(G1) = E(G2) then G1 = G2.

Русский

Графовая функция ребер инъективна: если E(G1) = E(G2), то G1 = G2.

LaTeX

$$$$ E(G_1) = E(G_2) \Rightarrow G_1 = G_2. $$$$

Lean4

theorem edgeSet_injective : Injective (edgeSet : SimpleGraph V → Set (Sym2 V)) :=
  (edgeSetEmbedding V).injective

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

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

Разделы

Аффилиация

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