subgraphOfAdj — Mathlib

English

Given an adjacency in G, the induced subgraph on the two endpoints is a matching.

Русский

Для смежности в G подграф на концевые вершины является соответствием.

LaTeX

$$$$ (G.subgraphOfAdj h).IsMatching $$$$

Lean4

theorem subgraphOfAdj (h : G.Adj v w) : (G.subgraphOfAdj h).IsMatching :=
  by
  intro _ hv
  rw [subgraphOfAdj_verts, Set.mem_insert_iff, Set.mem_singleton_iff] at hv
  cases hv with
  | inl => use w; aesop
  | inr => use v; aesop

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