toEdge_eq_of_adj — Mathlib

English

If a vertex v is adjacent to w under a matching h, then the edge produced by h for v equals the edge produced by h for w, up to symmetry of the edge.

Русский

Если вершина v смежна с w при совпадении h, ребро, получаемое для v, совпадает с ребром, получаемым для w, по симметрии ребра.

LaTeX

$$$$h.toEdge\\langle v, hv\\rangle = h.toEdge\\langle w, hw\\rangle$$$$

Lean4

theorem toEdge_eq_of_adj (h : M.IsMatching) (hv : v ∈ M.verts) (hvw : M.Adj v w) : h.toEdge ⟨v, hv⟩ = ⟨s(v, w), hvw⟩ :=
  by
  simp only [IsMatching.toEdge, Subtype.mk_eq_mk]
  congr
  exact ((h (M.edge_vert hvw)).choose_spec.2 w hvw).symm

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