eq_of_adj_left

Mathlib.Combinatorics.SimpleGraph.Matching

URI: https://scilib.ai/kg/mathlib#SimpleGraph.Subgraph.IsMatching.eq_of_adj_left

English

If h is a matching and adjacent edges hv and huv, then u and v are adjacent in the unique sense given by h.

Русский

Если h — соответствие и hv, hu, то u и v смежны в единственном смысле, заданном h.

LaTeX

$$$$ h.M^{\\mathrm{edge}}(u,v) $$$$

Lean4

theorem eq_of_adj_left (hM : M.IsMatching) (huv : M.Adj u v) (huw : M.Adj u w) : v = w :=
  (hM <| M.edge_vert huv).unique huv huw

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

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

Разделы

Аффилиация

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