eq_of_adj_right

Mathlib.Combinatorics.SimpleGraph.Matching

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

English

Symmetry of the previous statement: if huw and hvw, then u and v are equal via the left version.

Русский

Симметрия предыдущего утверждения: если huw и hvw, то u и v эквивалентны по левой версии.

LaTeX

$$$$ h.eq_of_adj_right (huw) (hvw) $$$$

Lean4

theorem eq_of_adj_right (hM : M.IsMatching) (huw : M.Adj u w) (hvw : M.Adj v w) : u = v :=
  hM.eq_of_adj_left huw.symm hvw.symm

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

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

Разделы

Аффилиация

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