subgraphOfAdj_le_of_adj — Mathlib

English

For any subgraph H of G and any hvw with hvw an edge in H, the subgraph of G determined by that edge is contained in H.

Русский

Для любой подграфа H графа G и для hvw, являющегося ребром в H, подграф G.subgraphOfAdj hvw содержится в H.

LaTeX

$$$G.\\mathrm{subgraphOfAdj}(H.\\mathrm{adj_sub} h) \\le H$$$

Lean4

theorem subgraphOfAdj_le_of_adj {v w : V} (H : G.Subgraph) (h : H.Adj v w) : G.subgraphOfAdj (H.adj_sub h) ≤ H :=
  by
  constructor
  · intro x
    rintro (rfl | rfl) <;> simp [H.edge_vert h, H.edge_vert h.symm]
  · simp only [subgraphOfAdj_adj, Sym2.eq, Sym2.rel_iff]
    rintro _ _ (⟨rfl, rfl⟩ | ⟨rfl, rfl⟩) <;> simp [h, h.symm]

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