support_subgraphOfAdj — Mathlib

English

The operation Subgraph.coeSubgraph composes a co-subgraph with the map that embeds it into a larger graph.

Русский

Операция Subgraph.coeSubgraph составляется с встроенным отображением в больший граф.

LaTeX

$$$\\mathrm{Subgraph.coeSubgraph}(G') = \\mathrm{Subgraph.map}(G'.hom)$$$

Lean4

@[simp]
theorem support_subgraphOfAdj {u v : V} (h : G.Adj u v) : (G.subgraphOfAdj h).support = { u, v } :=
  by
  ext
  rw [Subgraph.mem_support]
  simp only [subgraphOfAdj_adj, Sym2.eq, Sym2.rel_iff', Prod.mk.injEq, Prod.swap_prod_mk]
  refine ⟨?_, fun h ↦ h.elim (fun hl ↦ ⟨v, .inl ⟨hl.symm, rfl⟩⟩) fun hr ↦ ⟨u, .inr ⟨rfl, hr.symm⟩⟩⟩
  rintro ⟨_, hw⟩
  exact hw.elim (fun h1 ↦ .inl h1.1.symm) fun hr ↦ .inr hr.2.symm

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