adj_congr_of_sym2

Mathlib.Combinatorics.SimpleGraph.Basic

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

← MathLib Explorer

English

If s(u,v) = s(w,x), then G.Adj u v ↔ G.Adj w x.

Русский

Если s(u,v) = s(w,x), то G.Adj u v ↔ G.Adj w x.

LaTeX

$$$ s(u,v) = s(w,x) \Rightarrow G.Adj u v \iff G.Adj w x $$$

Lean4

theorem adj_congr_of_sym2 {u v w x : V} (h : s(u, v) = s(w, x)) : G.Adj u v ↔ G.Adj w x :=
  by
  simp only [Sym2.eq, Sym2.rel_iff', Prod.mk.injEq, Prod.swap_prod_mk] at h
  rcases h with hl | hr
  · rw [hl.1, hl.2]
  · rw [hr.1, hr.2, adj_comm]

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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