subgraphOfAdj_symm — Mathlib

English

The subgraph of adjacency hvw is unchanged when the endpoints are swapped: G.subgraphOfAdj hvw = G.subgraphOfAdj hvw.symm.

Русский

Подграф смежности hvw не меняется, если поменять концы; G.subgraphOfAdj hvw = G.subgraphOfAdj hvw.symm.

LaTeX

$$$G.\\mathrm{subgraphOfAdj}(hvw) = G.\\mathrm{subgraphOfAdj}(hvw.first.symm)$$$

Lean4

theorem subgraphOfAdj_symm {v w : V} (hvw : G.Adj v w) : G.subgraphOfAdj hvw.symm = G.subgraphOfAdj hvw := by
  ext <;> simp [or_comm, and_comm]

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